Changeset 700 for src/ASM/BitVector.ma
 Timestamp:
 Mar 18, 2011, 4:28:26 PM (9 years ago)
 File:

 1 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 ≝
Note: See TracChangeset
for help on using the changeset viewer.