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

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list.ma b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
index 7864ed0ab..781fc27a5 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
@@ -19,15 +19,20 @@ include "ground/lib/relations.ma".
 (* LISTS ********************************************************************)
 
 inductive list (A:Type[0]) : Type[0] :=
-  | nil : list A
-  | cons: A → list A → list A.
+| list_nil : list A
+| list_cons: A → list A → list A
+.
 
-interpretation "nil (list)" 'CircledE A = (nil A).
+interpretation
+  "nil (lists)"
+  'CircledE A = (list_nil A).
 
-interpretation "cons (list)" 'OPlusRight A hd tl = (cons A hd tl).
+interpretation
+  "cons (lists)"
+  'OPlusRight A hd tl = (list_cons A hd tl).
 
-rec definition all A (R:predicate A) (l:list A) on l ≝
-  match l with
-  [ nil        ⇒ ⊤
-  | cons hd tl ⇒ ∧∧ R hd & all A R 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
+].