X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FGround_2%2Flist.ma;h=0a6e69bbee01308d429c242af9e17469b855b3c5;hb=b5db76fe31ab35bae0257cb6684c511bcc531e45;hp=9bdc5c1260552ea92d82c5f0e135bce6cdfdbe09;hpb=78f21d7d9014e5c7655f58239e4f1a128ea2c558;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 9bdc5c126..0a6e69bbe 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/list.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/list.ma
@@ -13,22 +13,43 @@
 (**************************************************************************)
 
 include "Ground_2/arith.ma".
-include "Ground_2/notation.ma".
 
 (* LISTS ********************************************************************)
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil : list A
-  | cons: A -> list A -> list A.
+  | cons: A → list A → list A.
 
 interpretation "nil (list)" 'Nil = (nil ?).
 
 interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
 
-let rec append A (l1: list A) l2 on l1 ≝ 
-  match l1 with
-  [ nil        ⇒  l2
-  | cons hd tl ⇒  hd :: append A tl l2
+let rec all A (R:predicate A) (l:list A) on l ≝
+  match l with
+  [ nil        ⇒ True
+  | cons hd tl ⇒ R hd ∧ all A R tl
   ].
 
-interpretation "append (list)" 'Append l1 l2 = (append ? l1 l2).
+inductive list2 (A1,A2:Type[0]) : Type[0] :=
+  | nil2 : list2 A1 A2
+  | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2.
+
+interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?).
+
+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).