Empty types not in Prop and empty types elimination handled correctly.

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

diff --git a/matita/library/list/list.ma b/matita/library/list/list.ma
index f214ff3efa11b6b2559bfa302f2d5dfb4174495d..f832d502002f3c9a59855a13acea0ac966fa69bc 100644 (file)
--- 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'
+  ].