X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flist%2Flist.ma;h=f832d502002f3c9a59855a13acea0ac966fa69bc;hb=73044fcac2ab47e6c9819c572f6bbd2b1e0f2a40;hp=f214ff3efa11b6b2559bfa302f2d5dfb4174495d;hpb=86bb723de51760e2b62d365b31b79e28615f430e;p=helm.git

diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index f214ff3ef..f832d5020 100644
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/matita/library/list/list.ma
@@ -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'
+  ].