Changeset 229 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 9, 2010, 5:00:50 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r228 r229 5 5 include "Cartesian.ma". 6 6 include "Nat.ma". 7 include "Util.ma". 7 8 (* include "List.ma". *) 8 9 … … 44 45 match v with 45 46 [ Empty ⇒ Z 46  Cons n hd tl ⇒ S (length A n tl)47  Cons n hd tl ⇒ S $ length A n tl 47 48 ]. 48 49 … … 69 70 nqed. 70 71 71 72 72 nlet rec zip (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat) 73 73 (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝ … … 77 77 match q return (λy.λr. S n = y → Vector C (S n)) with 78 78 [ Empty ⇒ ? 79  Cons m hd 2 tl2⇒79  Cons m hd' tl' ⇒ 80 80 λe: S n = S m. 81 Cons C n (f hd hd2)(zip A B C n f tl ?)81 (f hd hd') :: (zip A B C n f tl ?) 82 82 ] 83 83 ]) … … 85 85 ## 86 86 [ #e; 87 ndestruct 87 ndestruct(e); 88 88 ## 89  ndestruct 90 napply tl 289  ndestruct(e); 90 napply tl' 91 91 ## 92 92 ]
Note: See TracChangeset
for help on using the changeset viewer.