Changeset 248 for Deliverables/D4.1/Matita/BitVector.ma
- Timestamp:
- Nov 22, 2010, 11:43:04 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/BitVector.ma
r246 r248 23 23 ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))). 24 24 ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))). 25 ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))). 25 26 26 27 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 196 197 | Cons o hd tl ⇒ 197 198 let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in 198 ((exponential (S (S Z)) o) ×hdval) + nat_of_bitvector o tl199 ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl 199 200 ].
Note: See TracChangeset
for help on using the changeset viewer.