Better notation, in particular for subset comprehension.

[helm.git] / helm / software / matita / core_notation.moo

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index ed0c7007beb4e5384bf19097347e689bef0e4c17..cceee24124153d236671b761b466f5af791afaa3 100644 (file)
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -11,6 +11,19 @@ notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
        }.
 
+notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
+  right associative with precedence 20
+for @{ 'sigma ${default
+  @{\lambda ${ident i} : $ty. $p}
+  @{\lambda ${ident i} . $p}}}.
+
+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)} } }
+       }.
+
 notation "hvbox(\langle term 19 a, break term 19 b\rangle)" 
 with precedence 90 for @{ 'pair $a $b}.
 
@@ -94,11 +107,15 @@ notation "hvbox(a break * b)"
   left associative with precedence 55
 for @{ 'times $a $b }.
 
+notation "hvbox(a break \middot b)" 
+  left associative with precedence 55
+  for @{ 'middot $a $b }.
+
 notation "hvbox(a break \mod b)" 
   left associative with precedence 55
 for @{ 'module $a $b }.
 
-notation "\frac a b" 
+notation "a \frac b" 
   non associative with precedence 90
 for @{ 'divide $a $b }.
 
@@ -117,10 +134,6 @@ notation "a !"
   non associative with precedence 80
 for @{ 'fact $a }.
 
-notation "(a \sup b)"
-  right associative with precedence 65
-for @{ 'exp $a $b}.
-
 notation "\sqrt a" 
   non associative with precedence 60
 for @{ 'sqrt $a }.
@@ -136,3 +149,68 @@ for @{ 'and $a $b }.
 notation "hvbox(\lnot a)" 
   non associative with precedence 40
 for @{ 'not $a }.
+
+notation > "hvbox(a break \liff b)" 
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)" 
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+
+notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70
+for @{ 'powerset $A }.
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
+
+notation "hvbox(a break ∈ b)" non associative with precedence 45
+for @{ 'mem $a $b }.
+
+notation "hvbox(a break ≬ b)" non associative with precedence 45
+for @{ 'overlaps $a $b }. (* \between *)
+
+notation "hvbox(a break ⊆ b)" non associative with precedence 45
+for @{ 'subseteq $a $b }. (* \subseteq *)
+
+notation "hvbox(a break ∩ b)" non associative with precedence 55
+for @{ 'intersects $a $b }. (* \cap *)
+
+notation "hvbox(a break ∪ b)" non associative with precedence 50
+for @{ 'union $a $b }. (* \cup *)
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+notation "hvbox(a break \approx b)" non associative with precedence 45 
+  for @{ 'napart $a $b}.
+        
+notation "hvbox(a break # b)" non associative with precedence 45 
+  for @{ 'apart $a $b}.
+    
+notation "hvbox(a break \circ b)" 
+  left associative with precedence 55
+for @{ 'compose $a $b }.
+
+notation "(a \sup b)" left associative with precedence 60 for @{ 'exp $a $b}.
+notation "s \sup (-1)" with precedence 60 for @{ 'invert $s }.
+notation < "s \sup (-1) x" with precedence 60 for @{ 'invert_appl $s $x}. 
+
+notation "hvbox(|term 90 C|)" with precedence 69 for @{ 'card $C }.
+
+notation "\naturals" non associative with precedence 90 for @{'N}.
+notation "\rationals" non associative with precedence 90 for @{'Q}.
+notation "\reals" non associative with precedence 90 for @{'R}.
+notation "\integers" non associative with precedence 90 for @{'Z}.
+notation "\complexes" non associative with precedence 90 for @{'C}.
+
+notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)