Changeset 535 for Deliverables/D3.1/Csemantics/cerco/BitVector.ma
 Timestamp:
 Feb 16, 2011, 4:25:02 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/cerco/BitVector.ma
r475 r535 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.