- we enabled a notation for ex2

[helm.git] / matita / matita / lib / basics / core_notation.ma

diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma
index 904adcd52f2fff140dd65eadb6e0945a219c4237..a37b4d8591fe6f4fd373ed6b88d59826acfe2f7b 100644 (file)
--- a/matita/matita/lib/basics/core_notation.ma
+++ b/matita/matita/lib/basics/core_notation.ma
@@ -27,6 +27,14 @@ notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
        }.
 
+notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'exists2 (λ${ident x0}.$P0) (λ${ident x0}.$P1) }.
+
+notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'exists2 (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) }.
+
 (* sigma ********************************************************************)
 
 notation < "hvbox(\Sigma ident i : ty break . p)"