Changeset 244 for Deliverables/D4.1/Matita/Vector.ma
- Timestamp:
- Nov 15, 2010, 10:42:20 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/Vector.ma
r243 r244 233 233 (v: Vector A n) on v ≝ 234 234 match v return λn.λv. List A with 235 [ Empty ⇒ ? (cic:/matita/Cerco/ Datatypes/Listlike/List/List/List.con(0,1,1) A)235 [ Empty ⇒ ? (cic:/matita/Cerco/List/List.con(0,1,1) A) 236 236 | Cons o hd tl ⇒ hd :: (list_of_vector A o tl) 237 237 ]. … … 241 241 nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝ 242 242 match l return λl. Vector A (length A l) with 243 [ Empty ⇒ ? (cic:/matita/Cerco/ Datatypes/Listlike/Vector/Vector/Vector.con(0,1,1) A)243 [ Empty ⇒ ? (cic:/matita/Cerco/Vector/Vector.con(0,1,1) A) 244 244 | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl)) 245 245 ].
Note: See TracChangeset
for help on using the changeset viewer.