Changeset 353 for Deliverables/D4.1/Matita/BitVector.ma
 Timestamp:
 Dec 1, 2010, 6:40:15 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r351 r353 166 166 vector_of_list Bool l. 167 167 168 nlet rec bitvector_of_nat_aux (n: Nat) on n ≝ 169 let divrem ≝ divide_with_remainder n (S (S Z)) in 170 let div ≝ first Nat Nat divrem in 171 let rem ≝ second Nat Nat divrem in 172 match div with 173 [ Z ⇒ 174 match rem with 175 [ Z ⇒ Empty Bool 176  S r ⇒ ? (true :: (bitvector_of_nat_aux Z)) 177 ] 178  S d ⇒ 179 match rem with 180 [ Z ⇒ ? (false :: (bitvector_of_nat_aux (S d))) 181  S r ⇒ ? (true :: (bitvector_of_nat_aux (S d))) 182 ] 183 ]. 184 //. 185 nqed. 168 nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝ 169 match bound with 170 [ Z ⇒ Empty Bool (* IT WILL NOT HAPPEN *) 171  S bound ⇒ 172 let divrem ≝ divide_with_remainder n (S (S Z)) in 173 let div ≝ first Nat Nat divrem in 174 let rem ≝ second Nat Nat divrem in 175 match div with 176 [ Z ⇒ 177 match rem with 178 [ Z ⇒ Empty Bool 179  S r ⇒ true :: (bitvector_of_nat_aux Z bound) 180 ] 181  S d ⇒ 182 match rem with 183 [ Z ⇒ false :: (bitvector_of_nat_aux (S d) bound) 184  S r ⇒ true :: (bitvector_of_nat_aux (S d) bound) 185 ] 186 ]]. 186 187 187 188 ndefinition eq_bv ≝ … … 196 197 197 198 nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝ 198 let biglist ≝ reverse ? (bitvector_of_nat_aux m ) in199 let biglist ≝ reverse ? (bitvector_of_nat_aux m m) in 199 200 let size ≝ length ? biglist in 200 201 let bitvector ≝ bitvector_of_list biglist in
Note: See TracChangeset
for help on using the changeset viewer.