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 notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
31 non associative with precedence 20
32 for @{ 'exists2 (λ${ident x0}.$P0) (λ${ident x0}.$P1) }.
34 notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
35 non associative with precedence 20
36 for @{ 'exists2 (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) }.
38 (* sigma ********************************************************************)
40 notation < "hvbox(\Sigma ident i : ty break . p)"
41 left associative with precedence 20
42 for @{'sigma (\lambda ${ident i} : $ty. $p) }.
44 notation < "hvbox(\Sigma ident i break . p)"
46 for @{'sigma (\lambda ${ident i}. $p) }.
49 notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
50 right associative with precedence 20
51 for @{ 'sigma ${default
52 @{\lambda ${ident i} : $ty. $p}
53 @{\lambda ${ident i} . $p}}}.
56 notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
59 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
60 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
63 notation "hvbox(« term 19 a, break term 19 b»)"
64 with precedence 90 for @{ 'dp $a $b }.
66 (* dependent pairs (i.e. Sigma with predicate in Type[0]) ********************)
68 notation < "hvbox(𝚺 ident i : ty break . p)"
69 left associative with precedence 20
70 for @{'dpair (\lambda ${ident i} : $ty. $p) }.
72 notation < "hvbox(𝚺 ident i break . p)"
74 for @{'dpair (\lambda ${ident i}. $p) }.
77 notation < "hvbox(𝚺 ident i opt (: ty) break . p)"
78 right associative with precedence 20
79 for @{ 'dpair ${default
80 @{\lambda ${ident i} : $ty. $p}
81 @{\lambda ${ident i} . $p}}}.
84 notation > "𝚺 list1 ident x sep , opt (: T). term 19 Px"
87 @{ ${ fold right @{$Px} rec acc @{'dpair (λ${ident x}:$T.$acc)} } }
88 @{ ${ fold right @{$Px} rec acc @{'dpair (λ${ident x}.$acc)} } }
91 notation "hvbox(❬ term 19 a, break term 19 b❭)"
92 with precedence 90 for @{ 'mk_DPair $a $b }.
94 (* equality, conguence ******************************************************)
96 notation > "hvbox(a break = b)"
97 non associative with precedence 45
100 notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)"
101 non associative with precedence 45
102 for @{ 'eq $t $a $b }.
104 notation > "hvbox(n break (≅ \sub term 90 p) m)"
105 non associative with precedence 45
106 for @{ 'congruent $n $m $p }.
108 notation < "hvbox(term 46 n break ≅ \sub p term 46 m)"
109 non associative with precedence 45
110 for @{ 'congruent $n $m $p }.
112 (* pairs, projections *******************************************************)
114 notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
115 with precedence 90 for @{ 'pair $a $b}.
117 notation "hvbox(x break \times y)" with precedence 70
118 for @{ 'product $x $y}.
120 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
121 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
123 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
124 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
126 notation > "\fst" with precedence 90 for @{'pi1}.
127 notation > "\snd" with precedence 90 for @{'pi2}.
129 (* implication **************************************************************)
131 notation "hvbox(a break \to b)"
132 right associative with precedence 20
133 for @{ \forall $_:$a.$b }.
135 notation < "hvbox(a break \to b)"
136 right associative with precedence 20
137 for @{ \Pi $_:$a.$b }.
139 (* orders *******************************************************************)
141 notation "hvbox(a break \leq b)"
142 non associative with precedence 45
145 notation "hvbox(a break \geq b)"
146 non associative with precedence 45
149 notation "hvbox(a break \lt b)"
150 non associative with precedence 45
153 notation "hvbox(a break \gt b)"
154 non associative with precedence 45
157 (* negated equality *********************************************************)
159 notation > "hvbox(a break \neq b)"
160 non associative with precedence 45
161 for @{ 'neq ? $a $b }.
163 notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
164 non associative with precedence 45
165 for @{ 'neq $t $a $b }.
167 (* negated orders ***********************************************************)
169 notation "hvbox(a break \nleq b)"
170 non associative with precedence 45
171 for @{ 'nleq $a $b }.
173 notation "hvbox(a break \ngeq b)"
174 non associative with precedence 45
175 for @{ 'ngeq $a $b }.
177 notation "hvbox(a break \nless b)"
178 non associative with precedence 45
179 for @{ 'nless $a $b }.
181 notation "hvbox(a break \ngtr b)"
182 non associative with precedence 45
183 for @{ 'ngtr $a $b }.
185 (* divides, negated divides *************************************************)
187 notation "hvbox(a break \divides b)"
188 non associative with precedence 45
189 for @{ 'divides $a $b }.
191 notation "hvbox(a break \ndivides b)"
192 non associative with precedence 45
193 for @{ 'ndivides $a $b }.
195 (* arithmetics **************************************************************)
197 notation "hvbox(a break + b)"
198 left associative with precedence 55
199 for @{ 'plus $a $b }.
201 notation "hvbox(a break - b)"
202 left associative with precedence 55
203 for @{ 'minus $a $b }.
205 notation "hvbox(a break * b)"
206 left associative with precedence 60
207 for @{ 'times $a $b }.
209 notation "hvbox(a break \middot b)"
210 left associative with precedence 60
211 for @{ 'middot $a $b }.
213 notation "hvbox(a break \mod b)"
214 left associative with precedence 60
215 for @{ 'module $a $b }.
217 notation < "a \frac b"
218 non associative with precedence 90
219 for @{ 'divide $a $b }.
222 left associative with precedence 60
223 for @{ 'divide $a $b }.
225 notation "hvbox(a break / b)"
226 left associative with precedence 60
227 for @{ 'divide $a $b }.
229 notation "- term 65 a" with precedence 65
233 non associative with precedence 80
237 non associative with precedence 65
240 (* logical connectives ******************************************************)
242 notation "hvbox(a break \lor b)"
243 left associative with precedence 30
246 notation "hvbox(a break \land b)"
247 left associative with precedence 35
250 notation "hvbox(\lnot a)"
251 non associative with precedence 40
254 notation > "hvbox(a break \liff b)"
255 left associative with precedence 25
258 notation "hvbox(a break \leftrightarrow b)"
259 left associative with precedence 25
262 (* subsets ******************************************************************)
264 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
265 for @{ 'powerset $A }.
266 notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
267 for @{ 'powerset $A }.
269 notation < "hvbox({ ident i | term 19 p })" with precedence 90
270 for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
272 notation > "hvbox({ ident i | term 19 p })" with precedence 90
273 for @{ 'subset (\lambda ${ident i}. $p)}.
275 notation < "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
276 for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
278 notation > "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
279 for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
281 notation "hvbox(a break ∈ b)" non associative with precedence 45
284 notation "hvbox(a break ∉ b)" non associative with precedence 45
285 for @{ 'notmem $a $b }.
287 notation "hvbox(a break ≬ b)" non associative with precedence 45
288 for @{ 'overlaps $a $b }. (* \between *)
290 notation "hvbox(a break ⊆ b)" non associative with precedence 45
291 for @{ 'subseteq $a $b }. (* \subseteq *)
293 notation "hvbox(a break ∩ b)" left associative with precedence 60
294 for @{ 'intersects $a $b }. (* \cap *)
296 notation "hvbox(a break ∪ b)" left associative with precedence 55
297 for @{ 'union $a $b }. (* \cup *)
299 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
301 (* other notations **********************************************************)
303 notation "hvbox(a break \approx b)" non associative with precedence 45
304 for @{ 'napart $a $b}.
306 notation "hvbox(a break # b)" non associative with precedence 45
307 for @{ 'apart $a $b}.
309 notation "hvbox(a break \circ b)"
310 left associative with precedence 60
311 for @{ 'compose $a $b }.
313 notation < "↓ \ensp a" with precedence 60 for @{ 'downarrow $a }.
314 notation > "↓ a" with precedence 60 for @{ 'downarrow $a }.
316 notation "hvbox(U break ↓ V)" non associative with precedence 60 for @{ 'fintersects $U $V }.
318 notation "↑a" with precedence 60 for @{ 'uparrow $a }.
320 notation "hvbox(a break ↑ b)" with precedence 60 for @{ 'funion $a $b }.
322 notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
323 notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
324 notation > "a ^ term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
325 notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }.
326 notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
327 notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}.
329 notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
331 notation "\naturals" non associative with precedence 90 for @{'N}.
332 notation "\rationals" non associative with precedence 90 for @{'Q}.
333 notation "\reals" non associative with precedence 90 for @{'R}.
334 notation "\integers" non associative with precedence 90 for @{'Z}.
335 notation "\complexes" non associative with precedence 90 for @{'C}.
337 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
339 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
340 notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
341 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
342 notation > "⊩ " with precedence 65 for @{'Vdash ?}.
343 notation "(⊩ \sub term 90 c) " with precedence 65 for @{'Vdash $c}.
345 notation < "maction (mstyle color #ff0000 (…)) (t)"
346 non associative with precedence 90 for @{'hide $t}.