Changeset 260 for Deliverables/D4.1/Matita/BitVector.ma
 Timestamp:
 Nov 23, 2010, 2:30:10 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r257 r260 55 55 ndefinition zero ≝ 56 56 λn: Nat. 57 ((replicate Bool n False): BitVector n).57 ((replicate Bool n false): BitVector n). 58 58 59 59 ndefinition max ≝ 60 60 λn: Nat. 61 ((replicate Bool n True): BitVector n).61 ((replicate Bool n true): BitVector n). 62 62 63 63 ndefinition append ≝ … … 72 72 λm, n: Nat. 73 73 λb: BitVector n. 74 let padding ≝ replicate Bool m False in74 let padding ≝ replicate Bool m false in 75 75 append Bool m n padding b. 76 76 … … 173 173 match rem with 174 174 [ Z ⇒ Empty Bool 175  S r ⇒ ? ( True :: (bitvector_of_nat_aux Z))175  S r ⇒ ? (true :: (bitvector_of_nat_aux Z)) 176 176 ] 177 177  S d ⇒ 178 178 match rem with 179 [ Z ⇒ ? ( False :: (bitvector_of_nat_aux (S d)))180  S r ⇒ ? ( True :: (bitvector_of_nat_aux (S d)))179 [ Z ⇒ ? (false :: (bitvector_of_nat_aux (S d))) 180  S r ⇒ ? (true :: (bitvector_of_nat_aux (S d))) 181 181 ] 182 182 ]. … … 196 196 [ Empty ⇒ Z 197 197  Cons o hd tl ⇒ 198 let hdval ≝ match hd with [ True ⇒ S Z  False ⇒ Z ] in198 let hdval ≝ match hd with [ true ⇒ S Z  false ⇒ Z ] in 199 199 ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl 200 200 ].
Note: See TracChangeset
for help on using the changeset viewer.