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 (* equality, conguence ******************************************************)
57 notation > "hvbox(a break = b)"
58 non associative with precedence 45
61 notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)"
62 non associative with precedence 45
63 for @{ 'eq $t $a $b }.
65 notation > "hvbox(n break (≅ \sub term 90 p) m)"
66 non associative with precedence 45
67 for @{ 'congruent $n $m $p }.
69 notation < "hvbox(term 46 n break ≅ \sub p term 46 m)"
70 non associative with precedence 45
71 for @{ 'congruent $n $m $p }.
73 (* other notations **********************************************************)
75 notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
76 with precedence 90 for @{ 'pair $a $b}.
78 notation "hvbox(x break \times y)" with precedence 70
79 for @{ 'product $x $y}.
81 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
82 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
84 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
85 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
87 notation > "\fst" with precedence 90 for @{'pi1}.
88 notation > "\snd" with precedence 90 for @{'pi2}.
90 notation "hvbox(a break \to b)"
91 right associative with precedence 20
92 for @{ \forall $_:$a.$b }.
94 notation < "hvbox(a break \to b)"
95 right associative with precedence 20
96 for @{ \Pi $_:$a.$b }.
98 notation "hvbox(a break \leq b)"
99 non associative with precedence 45
102 notation "hvbox(a break \geq b)"
103 non associative with precedence 45
106 notation "hvbox(a break \lt b)"
107 non associative with precedence 45
110 notation "hvbox(a break \gt b)"
111 non associative with precedence 45
114 notation > "hvbox(a break \neq b)"
115 non associative with precedence 45
116 for @{ 'neq ? $a $b }.
118 notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
119 non associative with precedence 45
120 for @{ 'neq $t $a $b }.
122 notation "hvbox(a break \nleq b)"
123 non associative with precedence 45
124 for @{ 'nleq $a $b }.
126 notation "hvbox(a break \ngeq b)"
127 non associative with precedence 45
128 for @{ 'ngeq $a $b }.
130 notation "hvbox(a break \nless b)"
131 non associative with precedence 45
132 for @{ 'nless $a $b }.
134 notation "hvbox(a break \ngtr b)"
135 non associative with precedence 45
136 for @{ 'ngtr $a $b }.
138 notation "hvbox(a break \divides b)"
139 non associative with precedence 45
140 for @{ 'divides $a $b }.
142 notation "hvbox(a break \ndivides b)"
143 non associative with precedence 45
144 for @{ 'ndivides $a $b }.
146 notation "hvbox(a break + b)"
147 left associative with precedence 50
148 for @{ 'plus $a $b }.
150 notation "hvbox(a break - b)"
151 left associative with precedence 50
152 for @{ 'minus $a $b }.
154 notation "hvbox(a break * b)"
155 left associative with precedence 55
156 for @{ 'times $a $b }.
158 notation "hvbox(a break \middot b)"
159 left associative with precedence 55
160 for @{ 'middot $a $b }.
162 notation "hvbox(a break \mod b)"
163 left associative with precedence 55
164 for @{ 'module $a $b }.
167 non associative with precedence 90
168 for @{ 'divide $a $b }.
171 left associative with precedence 55
172 for @{ 'divide $a $b }.
174 notation "hvbox(a break / b)"
175 left associative with precedence 55
176 for @{ 'divide $a $b }.
178 notation "- term 60 a" with precedence 60
182 non associative with precedence 80
186 non associative with precedence 60
189 notation "hvbox(a break \lor b)"
190 left associative with precedence 30
193 notation "hvbox(a break \land b)"
194 left associative with precedence 35
197 notation "hvbox(\lnot a)"
198 non associative with precedence 40
201 notation > "hvbox(a break \liff b)"
202 left associative with precedence 25
205 notation "hvbox(a break \leftrightarrow b)"
206 left associative with precedence 25
210 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70
211 for @{ 'powerset $A }.
213 notation < "hvbox({ ident i | term 19 p })" with precedence 90
214 for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
216 notation > "hvbox({ ident i | term 19 p })" with precedence 90
217 for @{ 'subset (\lambda ${ident i}. $p)}.
219 notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
220 for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
222 notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
223 for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
225 notation "hvbox(a break ∈ b)" non associative with precedence 45
228 notation "hvbox(a break ≬ b)" non associative with precedence 45
229 for @{ 'overlaps $a $b }. (* \between *)
231 notation "hvbox(a break ⊆ b)" non associative with precedence 45
232 for @{ 'subseteq $a $b }. (* \subseteq *)
234 notation "hvbox(a break ∩ b)" non associative with precedence 55
235 for @{ 'intersects $a $b }. (* \cap *)
237 notation "hvbox(a break ∪ b)" non associative with precedence 50
238 for @{ 'union $a $b }. (* \cup *)
240 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
242 notation "hvbox(a break \approx b)" non associative with precedence 45
243 for @{ 'napart $a $b}.
245 notation "hvbox(a break # b)" non associative with precedence 45
246 for @{ 'apart $a $b}.
248 notation "hvbox(a break \circ b)"
249 left associative with precedence 55
250 for @{ 'compose $a $b }.
252 notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
253 notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
255 notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
257 notation "↑a" with precedence 55 for @{ 'uparrow $a }.
259 notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
261 notation < "term 91 a \sup term 90 b" with precedence 90 for @{ 'exp $a $b}.
262 notation > "a \sup term 89 b" with precedence 90 for @{ 'exp $a $b}.
263 notation > "a ^ term 89 b" with precedence 90 for @{ 'exp $a $b}.
264 notation "s \sup (-1)" with precedence 90 for @{ 'invert $s }.
265 notation > "s ^ (-1)" with precedence 90 for @{ 'invert $s }.
266 notation < "s \sup (-1) x" with precedence 90 for @{ 'invert_appl $s $x}.
268 notation "hvbox(|term 90 C|)" with precedence 69 for @{ 'card $C }.
270 notation "\naturals" non associative with precedence 90 for @{'N}.
271 notation "\rationals" non associative with precedence 90 for @{'Q}.
272 notation "\reals" non associative with precedence 90 for @{'R}.
273 notation "\integers" non associative with precedence 90 for @{'Z}.
274 notation "\complexes" non associative with precedence 90 for @{'C}.
276 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
278 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
279 notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
280 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
281 notation > "⊩ " with precedence 60 for @{'Vdash ?}.
282 notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
284 notation < "maction (mstyle color #ff0000 (…)) (t)"
285 non associative with precedence 90 for @{'hide $t}.