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.