1 (* exists *******************************************************************)
3 notation "hvbox(∃ _ break . p)"
7 notation < "hvbox(\exists ident i : ty break . p)"
8 right associative with precedence 20
9 for @{'exists (\lambda ${ident i} : $ty. $p) }.
11 notation < "hvbox(\exists ident i break . p)"
13 for @{'exists (\lambda ${ident i}. $p) }.
16 notation < "hvbox(\exists ident i opt (: ty) break . p)"
17 right associative with precedence 20
18 for @{ 'exists ${default
19 @{\lambda ${ident i} : $ty. $p}
20 @{\lambda ${ident i} . $p}}}.
23 notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
26 @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
27 @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
30 (* sigma ********************************************************************)
32 notation < "hvbox(\Sigma ident i : ty break . p)"
33 left associative with precedence 20
34 for @{'sigma (\lambda ${ident i} : $ty. $p) }.
36 notation < "hvbox(\Sigma ident i break . p)"
38 for @{'sigma (\lambda ${ident i}. $p) }.
41 notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
42 right associative with precedence 20
43 for @{ 'sigma ${default
44 @{\lambda ${ident i} : $ty. $p}
45 @{\lambda ${ident i} . $p}}}.
48 notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
51 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
52 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
55 notation "hvbox(« term 19 a, break term 19 b»)"
56 with precedence 90 for @{ 'dp $a $b }.
58 (* dependent pairs (i.e. Sigma with predicate in Type[0]) ********************)
60 notation < "hvbox(𝚺 ident i : ty break . p)"
61 left associative with precedence 20
62 for @{'dpair (\lambda ${ident i} : $ty. $p) }.
64 notation < "hvbox(𝚺 ident i break . p)"
66 for @{'dpair (\lambda ${ident i}. $p) }.
69 notation < "hvbox(𝚺 ident i opt (: ty) break . p)"
70 right associative with precedence 20
71 for @{ 'dpair ${default
72 @{\lambda ${ident i} : $ty. $p}
73 @{\lambda ${ident i} . $p}}}.
76 notation > "𝚺 list1 ident x sep , opt (: T). term 19 Px"
79 @{ ${ fold right @{$Px} rec acc @{'dpair (λ${ident x}:$T.$acc)} } }
80 @{ ${ fold right @{$Px} rec acc @{'dpair (λ${ident x}.$acc)} } }
83 notation "hvbox(❬ term 19 a, break term 19 b❭)"
84 with precedence 90 for @{ 'mk_DPair $a $b }.
86 (* equality, conguence ******************************************************)
88 notation > "hvbox(a break = b)"
89 non associative with precedence 45
92 notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)"
93 non associative with precedence 45
94 for @{ 'eq $t $a $b }.
96 notation > "hvbox(n break (≅ \sub term 90 p) m)"
97 non associative with precedence 45
98 for @{ 'congruent $n $m $p }.
100 notation < "hvbox(term 46 n break ≅ \sub p term 46 m)"
101 non associative with precedence 45
102 for @{ 'congruent $n $m $p }.
104 (* other notations **********************************************************)
106 notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
107 with precedence 90 for @{ 'pair $a $b}.
109 notation "hvbox(x break \times y)" with precedence 70
110 for @{ 'product $x $y}.
112 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
113 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
115 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
116 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
118 notation > "\fst" with precedence 90 for @{'pi1}.
119 notation > "\snd" with precedence 90 for @{'pi2}.
121 notation "hvbox(a break \to b)"
122 right associative with precedence 20
123 for @{ \forall $_:$a.$b }.
125 notation < "hvbox(a break \to b)"
126 right associative with precedence 20
127 for @{ \Pi $_:$a.$b }.
129 notation "hvbox(a break \leq b)"
130 non associative with precedence 45
133 notation "hvbox(a break \geq b)"
134 non associative with precedence 45
137 notation "hvbox(a break \lt b)"
138 non associative with precedence 45
141 notation "hvbox(a break \gt b)"
142 non associative with precedence 45
145 notation > "hvbox(a break \neq b)"
146 non associative with precedence 45
147 for @{ 'neq ? $a $b }.
149 notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
150 non associative with precedence 45
151 for @{ 'neq $t $a $b }.
153 notation "hvbox(a break \nleq b)"
154 non associative with precedence 45
155 for @{ 'nleq $a $b }.
157 notation "hvbox(a break \ngeq b)"
158 non associative with precedence 45
159 for @{ 'ngeq $a $b }.
161 notation "hvbox(a break \nless b)"
162 non associative with precedence 45
163 for @{ 'nless $a $b }.
165 notation "hvbox(a break \ngtr b)"
166 non associative with precedence 45
167 for @{ 'ngtr $a $b }.
169 notation "hvbox(a break \divides b)"
170 non associative with precedence 45
171 for @{ 'divides $a $b }.
173 notation "hvbox(a break \ndivides b)"
174 non associative with precedence 45
175 for @{ 'ndivides $a $b }.
177 notation "hvbox(a break + b)"
178 left associative with precedence 50
179 for @{ 'plus $a $b }.
181 notation "hvbox(a break - b)"
182 left associative with precedence 50
183 for @{ 'minus $a $b }.
185 notation "hvbox(a break * b)"
186 left associative with precedence 55
187 for @{ 'times $a $b }.
189 notation "hvbox(a break \middot b)"
190 left associative with precedence 55
191 for @{ 'middot $a $b }.
193 notation "hvbox(a break \mod b)"
194 left associative with precedence 55
195 for @{ 'module $a $b }.
197 notation < "a \frac b"
198 non associative with precedence 90
199 for @{ 'divide $a $b }.
202 left associative with precedence 55
203 for @{ 'divide $a $b }.
205 notation "hvbox(a break / b)"
206 left associative with precedence 55
207 for @{ 'divide $a $b }.
209 notation "- term 60 a" with precedence 60
213 non associative with precedence 80
217 non associative with precedence 60
220 notation "hvbox(a break \lor b)"
221 left associative with precedence 30
224 notation "hvbox(a break \land b)"
225 left associative with precedence 35
228 notation "hvbox(\lnot a)"
229 non associative with precedence 40
232 notation > "hvbox(a break \liff b)"
233 left associative with precedence 25
236 notation "hvbox(a break \leftrightarrow b)"
237 left associative with precedence 25
241 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
242 for @{ 'powerset $A }.
243 notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
244 for @{ 'powerset $A }.
246 notation < "hvbox({ ident i | term 19 p })" with precedence 90
247 for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
249 notation > "hvbox({ ident i | term 19 p })" with precedence 90
250 for @{ 'subset (\lambda ${ident i}. $p)}.
252 notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
253 for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
255 notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
256 for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
258 notation "hvbox(a break ∈ b)" non associative with precedence 45
261 notation "hvbox(a break ≬ b)" non associative with precedence 45
262 for @{ 'overlaps $a $b }. (* \between *)
264 notation "hvbox(a break ⊆ b)" non associative with precedence 45
265 for @{ 'subseteq $a $b }. (* \subseteq *)
267 notation "hvbox(a break ∩ b)" left associative with precedence 55
268 for @{ 'intersects $a $b }. (* \cap *)
270 notation "hvbox(a break ∪ b)" left associative with precedence 50
271 for @{ 'union $a $b }. (* \cup *)
273 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
275 notation "hvbox(a break \approx b)" non associative with precedence 45
276 for @{ 'napart $a $b}.
278 notation "hvbox(a break # b)" non associative with precedence 45
279 for @{ 'apart $a $b}.
281 notation "hvbox(a break \circ b)"
282 left associative with precedence 55
283 for @{ 'compose $a $b }.
285 notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
286 notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
288 notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
290 notation "↑a" with precedence 55 for @{ 'uparrow $a }.
292 notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
294 notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
295 notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
296 notation > "a ^ term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
297 notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }.
298 notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
299 notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}.
301 notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
303 notation "\naturals" non associative with precedence 90 for @{'N}.
304 notation "\rationals" non associative with precedence 90 for @{'Q}.
305 notation "\reals" non associative with precedence 90 for @{'R}.
306 notation "\integers" non associative with precedence 90 for @{'Z}.
307 notation "\complexes" non associative with precedence 90 for @{'C}.
309 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
311 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
312 notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
313 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
314 notation > "⊩ " with precedence 60 for @{'Vdash ?}.
315 notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
317 notation < "maction (mstyle color #ff0000 (…)) (t)"
318 non associative with precedence 90 for @{'hide $t}.