X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Flist.ma;h=e72b54531a68816777ebcab50614b146f8c87bbe;hb=5102e7f780e83c7fef1d3826f81dfd37ee4028bc;hp=9355f9c56185175fa263fba844548e432a7672f9;hpb=174ee1889b5c91ef5339c718d7657ed0e5da21e8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
index 9355f9c56..e72b54531 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
@@ -28,6 +28,14 @@ interpretation "nil (list)" 'Nil = (nil ?).
 
 interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
 
+let rec length (A:Type[0]) (l:list A) on l ≝ match l with
+[ nil      ⇒ 0
+| cons _ l ⇒ length A l + 1
+].
+
+interpretation "length (list)"
+   'card l = (length ? l).
+
 let rec all A (R:predicate A) (l:list A) on l ≝
   match l with
   [ nil        ⇒ ⊤