Changeset 698 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Mar 18, 2011, 1:47:53 PM (9 years ago)
Author:
mulligan
Message:

Commit with changes to files to get our files to typecheck.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r697 r698  
    88include "arithmetics/nat.ma".
    99
    10 include "cerco/Util.ma".
    11 include "cerco/Vector.ma".
    12 include "cerco/String.ma".
     10include "ASM/Util.ma".
     11include "ASM/Vector.ma".
     12include "ASM/String.ma".
    1313
    1414(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    123123        false) b c.
    124124
     125(* dpm: commented out to get our stuff to typecheck
    125126lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y.
    126127  (x = y → P true) →
     
    130131#Q * *; normalize /3/
    131132qed.
     133*)
    132134
    133135let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝
Note: See TracChangeset for help on using the changeset viewer.