X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcore_notation.moo;h=be61e665096eb7f346ff55f4fae9f55fe54638c1;hb=d3548c16f481b14ce94e64c790bc767c59590050;hp=94b38082be07c401f72fcf198a78f03d48fbb581;hpb=f524a0d716de2bdc0874aace8f82f6289034eccf;p=helm.git

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index 94b38082b..be61e6650 100644
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -1,44 +1,36 @@
 (* exists *******************************************************************)
 
-notation < "hvbox(\exists ident i : ty break . p)"
+notation "hvbox(∃ _ break . p)"
  with precedence 20
+for @{'exists $p }.
+
+notation < "hvbox(\exists ident i : ty break . p)"
+ right associative with precedence 20
 for @{'exists (\lambda ${ident i} : $ty. $p) }.
 
 notation < "hvbox(\exists ident i break . p)"
- with precedence 20
+  with precedence 20
 for @{'exists (\lambda ${ident i}. $p) }.
 
 (*
 notation < "hvbox(\exists ident i opt (: ty) break . p)"
-  with precedence 20
+  right associative with precedence 20
 for @{ 'exists ${default
   @{\lambda ${ident i} : $ty. $p}
   @{\lambda ${ident i} . $p}}}.
 *)
 
-notation > "\exists list1 ident x sep , : T. term 19 Px"
-  with precedence 20
-for 
-  @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }.
-
-notation > "\exists list1 ident x sep , . term 19 Px"
-  with precedence 20
-for 
-  @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }.
-
-(*
 notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
   with precedence 20
   for ${ default
           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
        }.
-*)
 
 (* sigma ********************************************************************)
 
 notation < "hvbox(\Sigma ident i : ty break . p)"
- with precedence 20
+ left associative with precedence 20
 for @{'sigma (\lambda ${ident i} : $ty. $p) }.
 
 notation < "hvbox(\Sigma ident i break . p)"
@@ -47,30 +39,18 @@ for @{'sigma (\lambda ${ident i}. $p) }.
 
 (*
 notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
-  with precedence 20
+  right associative with precedence 20
 for @{ 'sigma ${default
   @{\lambda ${ident i} : $ty. $p}
   @{\lambda ${ident i} . $p}}}.
 *)
 
-notation > "\Sigma list1 ident x sep , : T. term 19 Px"
-  with precedence 20
-for 
-  @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }.
-
-notation > "\Sigma list1 ident x sep , . term 19 Px"
-  with precedence 20
-for 
-  @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }.
-
-(*
 notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
   with precedence 20
   for ${ default
           @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
           @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
        }.
-*)
 
 (* other notations **********************************************************)