Changeset 698 for src/ASM/BitVector.ma
 Timestamp:
 Mar 18, 2011, 1:47:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVector.ma
r697 r698 8 8 include "arithmetics/nat.ma". 9 9 10 include " cerco/Util.ma".11 include " cerco/Vector.ma".12 include " cerco/String.ma".10 include "ASM/Util.ma". 11 include "ASM/Vector.ma". 12 include "ASM/String.ma". 13 13 14 14 (* ===================================== *) … … 123 123 false) b c. 124 124 125 (* dpm: commented out to get our stuff to typecheck 125 126 lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y. 126 127 (x = y → P true) → … … 130 131 #Q * *; normalize /3/ 131 132 qed. 133 *) 132 134 133 135 let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝
Note: See TracChangeset
for help on using the changeset viewer.