X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FGround_2%2Flist.ma;h=883a8a8baa7a8cc7eb899048e3c1fc00fb44534c;hb=b5a168bec5e813258c510a1f2a00ce9f57ecee5a;hp=09a52f57d4c8bb8bc6719cb1bfc2672d8dd8c037;hpb=7e6643f9ce7ae87e9241aeac5b6d828e9d47fb63;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/list.ma b/matita/matita/contribs/lambda_delta/Ground_2/list.ma
index 09a52f57d..883a8a8ba 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/list.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/list.ma
@@ -45,3 +45,11 @@ let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
 
 interpretation "append (list of pairs)"
    'Append l1 l2 = (append2 ? ? l1 l2).
+
+let rec length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with
+[ nil2        ⇒ 0
+| cons2 _ _ l ⇒ length2 A1 A2 l + 1
+].
+
+interpretation "length (list of pairs)"
+   'card l = (length2 ? ? l).