]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/core_notation.moo
minor changes to make the library compile after wilmers new exists.
[helm.git] / helm / software / matita / core_notation.moo
1 notation < "hvbox(\exists ident i opt (: ty) break . p)"
2   right associative with precedence 20
3 for @{ 'exists ${default
4   @{\lambda ${ident i} : $ty. $p}
5   @{\lambda ${ident i} . $p}}}.
6
7 notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
8   with precedence 20
9   for ${ default
10           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
11           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
12        }.
13
14 notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
15   right associative with precedence 20
16 for @{ 'sigma ${default
17   @{\lambda ${ident i} : $ty. $p}
18   @{\lambda ${ident i} . $p}}}.
19
20 notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
21   with precedence 20
22   for ${ default
23           @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
24           @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
25        }.
26
27 notation "hvbox(\langle term 19 a, break term 19 b\rangle)" 
28 with precedence 90 for @{ 'pair $a $b}.
29
30 notation "hvbox(x break \times y)" with precedence 70
31 for @{ 'product $x $y}.
32
33 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
34 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
35
36 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
37 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
38
39 notation > "\fst" with precedence 90 for @{'pi1}.
40 notation > "\snd" with precedence 90 for @{'pi2}.
41
42 notation "hvbox(a break \to b)" 
43   right associative with precedence 20
44 for @{ \forall $_:$a.$b }.
45
46 notation < "hvbox(a break \to b)" 
47   right associative with precedence 20
48 for @{ \Pi $_:$a.$b }.
49
50 notation > "hvbox(a break = b)" 
51   non associative with precedence 45
52 for @{ 'eq ? $a $b }.
53 notation < "hvbox(a break maction (=) (=\sub t) b)" 
54   non associative with precedence 45
55 for @{ 'eq $t $a $b }.
56
57 notation "hvbox(a break \leq b)" 
58   non associative with precedence 45
59 for @{ 'leq $a $b }.
60
61 notation "hvbox(a break \geq b)" 
62   non associative with precedence 45
63 for @{ 'geq $a $b }.
64
65 notation "hvbox(a break \lt b)" 
66   non associative with precedence 45
67 for @{ 'lt $a $b }.
68
69 notation "hvbox(a break \gt b)" 
70   non associative with precedence 45
71 for @{ 'gt $a $b }.
72
73 notation > "hvbox(a break \neq b)" 
74   non associative with precedence 45
75 for @{ 'neq ? $a $b }.
76
77 notation < "hvbox(a break maction (\neq) (\neq\sub t) b)" 
78   non associative with precedence 45
79 for @{ 'neq $t $a $b }.
80
81 notation "hvbox(a break \nleq b)" 
82   non associative with precedence 45
83 for @{ 'nleq $a $b }.
84
85 notation "hvbox(a break \ngeq b)" 
86   non associative with precedence 45
87 for @{ 'ngeq $a $b }.
88
89 notation "hvbox(a break \nless b)" 
90   non associative with precedence 45
91 for @{ 'nless $a $b }.
92
93 notation "hvbox(a break \ngtr b)" 
94   non associative with precedence 45
95 for @{ 'ngtr $a $b }.
96
97 notation "hvbox(a break \divides b)"
98   non associative with precedence 45
99 for @{ 'divides $a $b }.
100
101 notation "hvbox(a break \ndivides b)"
102   non associative with precedence 45
103 for @{ 'ndivides $a $b }.
104
105 notation "hvbox(a break + b)" 
106   left associative with precedence 50
107 for @{ 'plus $a $b }.
108
109 notation "hvbox(a break - b)" 
110   left associative with precedence 50
111 for @{ 'minus $a $b }.
112
113 notation "hvbox(a break * b)" 
114   left associative with precedence 55
115 for @{ 'times $a $b }.
116
117 notation "hvbox(a break \middot b)" 
118   left associative with precedence 55
119   for @{ 'middot $a $b }.
120
121 notation "hvbox(a break \mod b)" 
122   left associative with precedence 55
123 for @{ 'module $a $b }.
124
125 notation "a \frac b" 
126   non associative with precedence 90
127 for @{ 'divide $a $b }.
128
129 notation "a \over b" 
130   left associative with precedence 55
131 for @{ 'divide $a $b }.
132
133 notation "hvbox(a break / b)" 
134   left associative with precedence 55
135 for @{ 'divide $a $b }.
136
137 notation "- term 60 a" with precedence 60 
138 for @{ 'uminus $a }.
139
140 notation "a !"
141   non associative with precedence 80
142 for @{ 'fact $a }.
143
144 notation "\sqrt a" 
145   non associative with precedence 60
146 for @{ 'sqrt $a }.
147
148 notation "hvbox(a break \lor b)" 
149   left associative with precedence 30
150 for @{ 'or $a $b }.
151
152 notation "hvbox(a break \land b)" 
153   left associative with precedence 35
154 for @{ 'and $a $b }.
155
156 notation "hvbox(\lnot a)" 
157   non associative with precedence 40
158 for @{ 'not $a }.
159
160 notation > "hvbox(a break \liff b)" 
161   left associative with precedence 25
162 for @{ 'iff $a $b }.
163
164 notation "hvbox(a break \leftrightarrow b)" 
165   left associative with precedence 25
166 for @{ 'iff $a $b }.
167
168
169 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70
170 for @{ 'powerset $A }.
171
172 notation < "hvbox({ ident i | term 19 p })" with precedence 90
173 for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
174
175 notation > "hvbox({ ident i | term 19 p })" with precedence 90
176 for @{ 'subset (\lambda ${ident i}. $p)}.
177
178 notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
179 for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
180
181 notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
182 for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
183
184 notation "hvbox(a break ∈ b)" non associative with precedence 45
185 for @{ 'mem $a $b }.
186
187 notation "hvbox(a break ≬ b)" non associative with precedence 45
188 for @{ 'overlaps $a $b }. (* \between *)
189
190 notation "hvbox(a break ⊆ b)" non associative with precedence 45
191 for @{ 'subseteq $a $b }. (* \subseteq *)
192
193 notation "hvbox(a break ∩ b)" non associative with precedence 55
194 for @{ 'intersects $a $b }. (* \cap *)
195
196 notation "hvbox(a break ∪ b)" non associative with precedence 50
197 for @{ 'union $a $b }. (* \cup *)
198
199 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
200
201 notation "hvbox(a break \approx b)" non associative with precedence 45 
202   for @{ 'napart $a $b}.
203         
204 notation "hvbox(a break # b)" non associative with precedence 45 
205   for @{ 'apart $a $b}.
206     
207 notation "hvbox(a break \circ b)" 
208   left associative with precedence 55
209 for @{ 'compose $a $b }.
210
211 notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
212 notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
213
214 notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
215
216 notation "↑a" with precedence 55 for @{ 'uparrow $a }.
217
218 notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
219
220 notation "a \sup term 89 b" with precedence 90 for @{ 'exp $a $b}.
221 notation > "a ^ term 89 b"  with precedence 90 for @{ 'exp $a $b}.
222 notation "s \sup (-1)" with precedence 90 for @{ 'invert $s }.
223 notation > "s ^ (-1)" with precedence 90 for @{ 'invert $s }.
224 notation < "s \sup (-1) x" with precedence 90 for @{ 'invert_appl $s $x}. 
225
226 notation "hvbox(|term 90 C|)" with precedence 69 for @{ 'card $C }.
227
228 notation "\naturals" non associative with precedence 90 for @{'N}.
229 notation "\rationals" non associative with precedence 90 for @{'Q}.
230 notation "\reals" non associative with precedence 90 for @{'R}.
231 notation "\integers" non associative with precedence 90 for @{'Z}.
232 notation "\complexes" non associative with precedence 90 for @{'C}.
233
234 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
235
236 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
237 notation > "x ⊩_term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
238 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
239 notation > "⊩ " with precedence 60 for @{'Vdash ?}.
240 notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
241
242 notation < "maction (mstyle color #ff0000 (­…­)) (t)" 
243 non associative with precedence 90 for @{'hide $t}.
244