Changeset 229
 Timestamp:
 Nov 9, 2010, 5:00:50 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 1 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/List.ma
r228 r229 1 1 include "Maybe.ma". 2 2 include "Nat.ma". 3 include "Util.ma". 3 4 4 5 ninductive List (A: Type[0]): Type[0] ≝ … … 20 21 match l with 21 22 [ Empty ⇒ Z 22  Cons hd tl ⇒ S (length A tl)23  Cons hd tl ⇒ S $ length A tl 23 24 ]. 24 25 … … 65 66 match l with 66 67 [ Empty ⇒ Empty A 67  Cons hd tl ⇒ reverse A tl @ ( Cons A hd (Empty A))68  Cons hd tl ⇒ reverse A tl @ (hd :: Empty A) 68 69 ]. 69 70 … … 87 88 match n with 88 89 [ Z ⇒ Empty A 89  S o ⇒ a :: (replicate A o a)90  S o ⇒ a :: replicate A o a 90 91 ]. 
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.