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=78a2305ea8dee7982f27c57203775de0911700af;hpb=a28bc89ee87228140c6559e3dacfeaaf2ac70d1d;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 78a2305ea..883a8a8ba 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/list.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/list.ma
@@ -37,3 +37,19 @@ inductive list2 (A1,A2:Type[0]) : Type[0] :=
 interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?). (**) (* 'Nil causes unification error in aacr_abst *)
 
 interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).
+
+let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
+[ nil2           ⇒ l2
+| cons2 a1 a2 tl ⇒ {a1, a2} :: append2 A1 A2 tl l2
+].
+
+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).