Changeset 268 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 23, 2010, 5:44:42 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r266 r268 5 5 6 6 include "Util.ma". 7 8 include "Universes.ma".9 7 10 8 include "Nat.ma". … … 133 131 ]. 134 132 //. 133 nqed. 134 135 nlet rec split (A: Type[0]) (n,m: Nat) on m 136 : Vector A (m+n) → (Vector A m) × (Vector A n) 137 ≝ 138 match m return λm. Vector A (m+n) → (Vector A m) × (Vector A n) with 139 [ Z ⇒ λv.〈[[ ]], v〉 140  S m' ⇒ λv. 141 match v return λl.λ_:Vector A l.l = S (m' + n) → (Vector A (S m')) × (Vector A n) with 142 [ Empty ⇒ λK.⊥ 143  Cons o he tl ⇒ λK. 144 match split A n m' (tl⌈Vector A (m'+n)↦Vector A o⌉) with 145 [ mk_Cartesian v1 v2 ⇒ 〈he::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))]. 146 //; ndestruct; //. 135 147 nqed. 136 148
Note: See TracChangeset
for help on using the changeset viewer.