Changeset 260 for Deliverables/D4.1/Matita/BitVector.ma
- Timestamp:
- Nov 23, 2010, 2:30:10 PM (10 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.