1 (* exists *******************************************************************)
3 notation < "hvbox(\exists ident i : ty break . p)"
5 for @{'exists (\lambda ${ident i} : $ty. $p) }.
7 notation < "hvbox(\exists ident i break . p)"
9 for @{'exists (\lambda ${ident i}. $p) }.
12 notation < "hvbox(\exists ident i opt (: ty) break . p)"
14 for @{ 'exists ${default
15 @{\lambda ${ident i} : $ty. $p}
16 @{\lambda ${ident i} . $p}}}.
19 notation > "\exists list1 ident x sep , : T. term 19 Px"
22 @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }.
24 notation > "\exists list1 ident x sep , . term 19 Px"
27 @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }.
30 notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
33 @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
34 @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
38 (* sigma ********************************************************************)
40 notation < "hvbox(\Sigma ident i : ty break . p)"
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)"
51 for @{ 'sigma ${default
52 @{\lambda ${ident i} : $ty. $p}
53 @{\lambda ${ident i} . $p}}}.
56 notation > "\Sigma list1 ident x sep , : T. term 19 Px"
59 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }.
61 notation > "\Sigma list1 ident x sep , . term 19 Px"
64 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }.
67 notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
70 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
71 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
75 (* other notations **********************************************************)
77 notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
78 with precedence 90 for @{ 'pair $a $b}.
80 notation "hvbox(x break \times y)" with precedence 70
81 for @{ 'product $x $y}.
83 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
84 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
86 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
87 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
89 notation > "\fst" with precedence 90 for @{'pi1}.
90 notation > "\snd" with precedence 90 for @{'pi2}.
92 notation "hvbox(a break \to b)"
93 right associative with precedence 20
94 for @{ \forall $_:$a.$b }.
96 notation < "hvbox(a break \to b)"
97 right associative with precedence 20
98 for @{ \Pi $_:$a.$b }.
100 notation > "hvbox(a break = b)"
101 non associative with precedence 45
102 for @{ 'eq ? $a $b }.
103 notation < "hvbox(a break maction (=) (=\sub t) b)"
104 non associative with precedence 45
105 for @{ 'eq $t $a $b }.
107 notation "hvbox(a break \leq b)"
108 non associative with precedence 45
111 notation "hvbox(a break \geq b)"
112 non associative with precedence 45
115 notation "hvbox(a break \lt b)"
116 non associative with precedence 45
119 notation "hvbox(a break \gt b)"
120 non associative with precedence 45
123 notation > "hvbox(a break \neq b)"
124 non associative with precedence 45
125 for @{ 'neq ? $a $b }.
127 notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
128 non associative with precedence 45
129 for @{ 'neq $t $a $b }.
131 notation "hvbox(a break \nleq b)"
132 non associative with precedence 45
133 for @{ 'nleq $a $b }.
135 notation "hvbox(a break \ngeq b)"
136 non associative with precedence 45
137 for @{ 'ngeq $a $b }.
139 notation "hvbox(a break \nless b)"
140 non associative with precedence 45
141 for @{ 'nless $a $b }.
143 notation "hvbox(a break \ngtr b)"
144 non associative with precedence 45
145 for @{ 'ngtr $a $b }.
147 notation "hvbox(a break \divides b)"
148 non associative with precedence 45
149 for @{ 'divides $a $b }.
151 notation "hvbox(a break \ndivides b)"
152 non associative with precedence 45
153 for @{ 'ndivides $a $b }.
155 notation "hvbox(a break + b)"
156 left associative with precedence 50
157 for @{ 'plus $a $b }.
159 notation "hvbox(a break - b)"
160 left associative with precedence 50
161 for @{ 'minus $a $b }.
163 notation "hvbox(a break * b)"
164 left associative with precedence 55
165 for @{ 'times $a $b }.
167 notation "hvbox(a break \middot b)"
168 left associative with precedence 55
169 for @{ 'middot $a $b }.
171 notation "hvbox(a break \mod b)"
172 left associative with precedence 55
173 for @{ 'module $a $b }.
176 non associative with precedence 90
177 for @{ 'divide $a $b }.
180 left associative with precedence 55
181 for @{ 'divide $a $b }.
183 notation "hvbox(a break / b)"
184 left associative with precedence 55
185 for @{ 'divide $a $b }.
187 notation "- term 60 a" with precedence 60
191 non associative with precedence 80
195 non associative with precedence 60
198 notation "hvbox(a break \lor b)"
199 left associative with precedence 30
202 notation "hvbox(a break \land b)"
203 left associative with precedence 35
206 notation "hvbox(\lnot a)"
207 non associative with precedence 40
210 notation > "hvbox(a break \liff b)"
211 left associative with precedence 25
214 notation "hvbox(a break \leftrightarrow b)"
215 left associative with precedence 25
219 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70
220 for @{ 'powerset $A }.
222 notation < "hvbox({ ident i | term 19 p })" with precedence 90
223 for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
225 notation > "hvbox({ ident i | term 19 p })" with precedence 90
226 for @{ 'subset (\lambda ${ident i}. $p)}.
228 notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
229 for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
231 notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
232 for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
234 notation "hvbox(a break ∈ b)" non associative with precedence 45
237 notation "hvbox(a break ≬ b)" non associative with precedence 45
238 for @{ 'overlaps $a $b }. (* \between *)
240 notation "hvbox(a break ⊆ b)" non associative with precedence 45
241 for @{ 'subseteq $a $b }. (* \subseteq *)
243 notation "hvbox(a break ∩ b)" non associative with precedence 55
244 for @{ 'intersects $a $b }. (* \cap *)
246 notation "hvbox(a break ∪ b)" non associative with precedence 50
247 for @{ 'union $a $b }. (* \cup *)
249 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
251 notation "hvbox(a break \approx b)" non associative with precedence 45
252 for @{ 'napart $a $b}.
254 notation "hvbox(a break # b)" non associative with precedence 45
255 for @{ 'apart $a $b}.
257 notation "hvbox(a break \circ b)"
258 left associative with precedence 55
259 for @{ 'compose $a $b }.
261 notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
262 notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
264 notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
266 notation "↑a" with precedence 55 for @{ 'uparrow $a }.
268 notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
270 notation "a \sup term 89 b" with precedence 90 for @{ 'exp $a $b}.
271 notation > "a ^ term 89 b" with precedence 90 for @{ 'exp $a $b}.
272 notation "s \sup (-1)" with precedence 90 for @{ 'invert $s }.
273 notation > "s ^ (-1)" with precedence 90 for @{ 'invert $s }.
274 notation < "s \sup (-1) x" with precedence 90 for @{ 'invert_appl $s $x}.
276 notation "hvbox(|term 90 C|)" with precedence 69 for @{ 'card $C }.
278 notation "\naturals" non associative with precedence 90 for @{'N}.
279 notation "\rationals" non associative with precedence 90 for @{'Q}.
280 notation "\reals" non associative with precedence 90 for @{'R}.
281 notation "\integers" non associative with precedence 90 for @{'Z}.
282 notation "\complexes" non associative with precedence 90 for @{'C}.
284 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
286 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
287 notation > "x ⊩_term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
288 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
289 notation > "⊩ " with precedence 60 for @{'Vdash ?}.
290 notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
292 notation < "maction (mstyle color #ff0000 (…)) (t)"
293 non associative with precedence 90 for @{'hide $t}.