Changeset 232 for Deliverables/D4.1/Matita/BitVector.ma
- Timestamp:
- Nov 11, 2010, 4:56:59 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/BitVector.ma
r231 r232 32 32 zip Bool Bool Bool n exclusive_disjunction b c. 33 33 34 nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal n m) ≝ 34 nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal_p n m): (BitVector (n + m)) ≝ 35 match m with 36 [ Z ⇒ ? 37 | S o ⇒ ? 38 ]. 39 40 //. 41 nqed. 42 43 ncheck pad. 35 44
Note: See TracChangeset
for help on using the changeset viewer.