X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Flist%2Flist.ma;h=f832d502002f3c9a59855a13acea0ac966fa69bc;hb=a5bfa65b18a876fca982270f673c686a7d124f65;hp=f214ff3efa11b6b2559bfa302f2d5dfb4174495d;hpb=8bb8d0afb6e8e82ffc84a2848bbb64e88ca03095;p=helm.git

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