Changeset 311 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 26, 2010, 1:28:13 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r272 r311 133 133 nqed. 134 134 135 nlet rec split (A: Type[0]) ( n,m: Nat) on m135 nlet rec split (A: Type[0]) (m,n: Nat) on m 136 136 : Vector A (m+n) → (Vector A m) × (Vector A n) 137 137 ≝ … … 142 142 [ Empty ⇒ λK.⊥ 143 143  Cons o he tl ⇒ λK. 144 match split A n m'(tl⌈Vector A (m'+n)↦Vector A o⌉) with144 match split A m' n (tl⌈Vector A (m'+n)↦Vector A o⌉) with 145 145 [ mk_Cartesian v1 v2 ⇒ 〈he::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))]. 146 146 //; ndestruct; //.
Note: See TracChangeset
for help on using the changeset viewer.