 Timestamp:
 Mar 18, 2011, 4:28:26 PM (9 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVector.ma
r698 r700 123 123 false) b c. 124 124 125 (* dpm: commented out to get our stuff to typecheck126 125 lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y. 127 126 (x = y → P true) → … … 131 130 #Q * *; normalize /3/ 132 131 qed. 133 *)134 132 135 133 let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝ 
src/ASM/BitVectorZ.ma
r697 r700 1 1 2 include " binary/Z.ma".3 include " cerco/BitVector.ma".4 include " cerco/Arithmetic.ma".2 include "utilities/binary/Z.ma". 3 include "ASM/BitVector.ma". 4 include "ASM/Arithmetic.ma". 5 5 6 6 let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝ 
src/ASM/Vector.ma
r698 r700 12 12 include "arithmetics/nat.ma". 13 13 14 (* include "oldlib/eq.ma". *) 14 include "utilities/oldlib/eq.ma". 15 15 16 16 (* ===================================== *) … … 469 469 *) 470 470 471 (* dpm: commented out to get out stuff to typecheck 471 (* dpm: commented out to get out stuff to typecheck *) 472 472 lemma eq_v_elim: ∀P:bool → Prop. ∀A,f. 473 473 (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) → … … 486 486 ] 487 487 ] qed. 488 *)489 488 490 489 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.