Changeset 697 for src/ASM/BitVector.ma
 Timestamp:
 Mar 18, 2011, 1:28:33 PM (9 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM

Property
svn:mergeinfo
set to
(toggle deleted branches)
/src/Clight/cerco merged eligible /Deliverables/D3.1/Csemantics/cerco 531693 /Deliverables/D4.1/Matita/newmatitadevelopment 476530

Property
svn:mergeinfo
set to
(toggle deleted branches)

src/ASM/BitVector.ma
r690 r697 123 123 false) b c. 124 124 125 lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y. 126 (x = y → P true) → 127 (x ≠ y → P false) → 128 P (eq_bv n x y). 129 #P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf) 130 #Q * *; normalize /3/ 131 qed. 132 125 133 let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝ 126 134 let biglist ≝ rev ? (bitvector_of_nat_aux m m) in
Note: See TracChangeset
for help on using the changeset viewer.