Changeset 236 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 12, 2010, 4:01:48 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r234 r236 159 159 (* ===================================== *) 160 160 161 nlet rec to_list(A: Type[0]) (n: Nat)162 (v: Vector A n) on v ≝163 match v with161 nlet rec list_of_vector (A: Type[0]) (n: Nat) 162 (v: Vector A n) on v ≝ 163 match v return λn.λv. List A with 164 164 [ Empty ⇒ cic:/matita/Cerco/List/List.con(0,1,1) A 165  Cons o hd tl ⇒ hd :: (to_listA o tl)165  Cons o hd tl ⇒ cic:/matita/Cerco/List/List.con(0,2,1) A hd (list_of_vector A o tl) 166 166 ]. 167 167 168 168 (* 169 nlet rec from_list (A: Type[0]) (l: List A) on l ≝169 nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝ 170 170 match l return λl. Vector A (length A l) with 171 171 [ Empty ⇒ cic:/matita/Cerco/Vector/Vector.con(0,1,1) A
Note: See TracChangeset
for help on using the changeset viewer.