Changeset 229 for Deliverables/D4.1/Matita/List.ma

Timestamp:

Nov 9, 2010, 5:00:50 PM (10 years ago)

Author:

mulligan

Message:

More changes.

File:

• Deliverables/D4.1/Matita/List.ma (modified) (4 diffs)

Deliverables/D4.1/Matita/List.ma

@@ -1 +1 @@
 include "Maybe.ma".
 include "Nat.ma".
+include "Util.ma".
 
 ninductive List (A: Type[0]): Type[0] ≝
@@ -20 +21 @@
   match l with
     [ Empty ⇒ Z
-    | Cons hd tl ⇒ S (length A tl)
+    | Cons hd tl ⇒ S $ length A tl
     ].
     
@@ -65 +66 @@
   match l with
     [ Empty ⇒ Empty A
-    | Cons hd tl ⇒ reverse A tl @ (Cons A hd (Empty A))
+    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
     ].
     
@@ -87 +88 @@
   match n with
     [ Z ⇒ Empty A
-    | S o ⇒ a :: (replicate A o a)
+    | S o ⇒ a :: replicate A o a
     ].