Changeset 271 for Deliverables/D4.1/Matita/BitVector.ma
- Timestamp:
- Nov 24, 2010, 1:00:41 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/BitVector.ma
r270 r271 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 ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S Z))))))))))). 26 26 27 27 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 200 200 ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl 201 201 ]. 202 202 203 (* 203 204 nlet rec equality (n: Nat) (b: BitVector n) (c: BitVector n) on b ≝ 204 205 match b with … … 209 210 | Cons 210 211 ]. 212 *)
Note: See TracChangeset
for help on using the changeset viewer.