X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Flist.ma;h=21a0f75602d53d5962585ffb0a7ac69d5480b7e3;hb=dd41efaab7f147d5673cc30a27d36375f9b52c9d;hp=781fc27a55791dde08660777837f20b879e9892e;hpb=6604a232815858a6c75dd25ac45abd68438077ff;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list.ma b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
index 781fc27a5..21a0f7560 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
@@ -18,21 +18,20 @@ include "ground/lib/relations.ma".
 
 (* LISTS ********************************************************************)
 
-inductive list (A:Type[0]) : Type[0] :=
-| list_nil : list A
-| list_cons: A → list A → list A
+inductive list (A:Type[0]): Type[0] :=
+| list_empty: list A
+| list_lcons: A → list A → list A
 .
 
 interpretation
-  "nil (lists)"
-  'CircledE A = (list_nil A).
+  "empty (lists)"
+  'CircledE A = (list_empty A).
 
 interpretation
-  "cons (lists)"
-  'OPlusRight A hd tl = (list_cons A hd tl).
+  "left cons (lists)"
+  'OPlusRight A hd tl = (list_lcons A hd tl).
 
-rec definition list_all A (R:predicate A) (l:list A) on l ≝
-match l with
-[ list_nil        ⇒ ⊤
-| list_cons hd tl ⇒ ∧∧ R hd & list_all A R tl
+rec definition list_all A (R:predicate A) (l:list A) on l ≝ match l with
+[ list_empty       ⇒ ⊤
+| list_lcons hd tl ⇒ ∧∧ R hd & list_all A R tl
 ].