Changeset 244 for Deliverables/D4.1/Matita/Vector.ma

Timestamp:

Nov 15, 2010, 10:42:20 AM (10 years ago)

Author:

mulligan

Message:

Vector.ma now compiles.

File:

• Deliverables/D4.1/Matita/Vector.ma (modified) (2 diffs)

Deliverables/D4.1/Matita/Vector.ma

@@ -233 +233 @@
                         (v: Vector A n) on v ≝
   match v return λn.λv. List A with
-    [ Empty ⇒ ? (cic:/matita/Cerco/Datatypes/Listlike/List/List/List.con(0,1,1) A)
+    [ Empty ⇒ ? (cic:/matita/Cerco/List/List.con(0,1,1) A)
     | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
     ].
@@ -241 +241 @@
 nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
   match l return λl. Vector A (length A l) with
-    [ Empty ⇒ ? (cic:/matita/Cerco/Datatypes/Listlike/Vector/Vector/Vector.con(0,1,1) A)
+    [ Empty ⇒ ? (cic:/matita/Cerco/Vector/Vector.con(0,1,1) A)
     | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
     ].