update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / list.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list.ma b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
index 7864ed0abfe41274f172e0b2be6b2e55f3d75d84..6dc752d65ad5b4aa84d5b22e2d6a8b9f0654e084 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
@@ -12,22 +12,26 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/circledE_1.ma".
+include "ground/notation/functions/circled_element_e_1.ma".
 include "ground/notation/functions/oplusright_3.ma".
 include "ground/lib/relations.ma".
 
 (* LISTS ********************************************************************)
 
-inductive list (A:Type[0]) : Type[0] :=
-  | nil : list A
-  | 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 (list)" 'CircledE A = (nil A).
+interpretation
+  "empty (lists)"
+  'CircledElementE A = (list_empty A).
 
-interpretation "cons (list)" 'OPlusRight A hd tl = (cons A hd tl).
+interpretation
+  "left cons (lists)"
+  'OPlusRight A hd tl = (list_lcons 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_empty       ⇒ ⊤
+| list_lcons hd tl ⇒ ∧∧ R hd & list_all A R tl
+].