LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES

[helm.git] / helm / software / matita / library / list / list.ma

diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index f214ff3efa11b6b2559bfa302f2d5dfb4174495d..ba4f61bc4b4e0aae11ef59f0ce74d40655c7cdc9 100644 (file)
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/matita/library/list/list.ma
@@ -32,9 +32,9 @@ notation "hvbox(l1 break @ l2)"
   right associative with precedence 47
   for @{'append $l1 $l2 }.
 
-interpretation "nil" 'nil = (cic:/matita/list/list.ind#xpointer(1/1/1) _).
+interpretation "nil" 'nil = (cic:/matita/list/list/list.ind#xpointer(1/1/1) _).
 interpretation "cons" 'cons hd tl =
-  (cic:/matita/list/list.ind#xpointer(1/1/2) _ hd tl).
+  (cic:/matita/list/list/list.ind#xpointer(1/1/2) _ hd tl).
 
 (* theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. *)
 
@@ -62,7 +62,7 @@ definition tail := \lambda A:Type. \lambda l: list A.
   [ nil => []
   | (cons hd tl) => tl].
 
-interpretation "append" 'append l1 l2 = (cic:/matita/list/append.con _ l1 l2).
+interpretation "append" 'append l1 l2 = (cic:/matita/list/list/append.con _ l1 l2).
 
 theorem append_nil: \forall A:Type.\forall l:list A.l @ [] = l.
   intros;
@@ -133,3 +133,13 @@ simplify.
 reflexivity.
 qed.
 *)
+
+let rec nth (A:Type) l d n on n ≝
+ match n with
+  [ O ⇒
+     match l with
+      [ nil ⇒ d
+      | cons (x : A) _ ⇒ x
+      ]
+  | S n' ⇒ nth A (tail ? l) d n'
+  ].