1 (* exists *******************************************************************)
3 notation < "hvbox(\exists ident i : ty break . p)"
4 right associative with precedence 20
5 for @{'exists (\lambda ${ident i} : $ty. $p) }.
7 notation < "hvbox(\exists ident i break . p)"
9 for @{'exists (\lambda ${ident i}. $p) }.
11 notation "hvbox(∃ _ break . 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 (* other notations **********************************************************)
57 notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
58 with precedence 90 for @{ 'pair $a $b}.
60 notation "hvbox(x break \times y)" with precedence 70
61 for @{ 'product $x $y}.
63 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
64 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
66 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
67 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
69 notation > "\fst" with precedence 90 for @{'pi1}.
70 notation > "\snd" with precedence 90 for @{'pi2}.
72 notation "hvbox(a break \to b)"
73 right associative with precedence 20
74 for @{ \forall $_:$a.$b }.
76 notation < "hvbox(a break \to b)"
77 right associative with precedence 20
78 for @{ \Pi $_:$a.$b }.
80 notation > "hvbox(a break = b)"
81 non associative with precedence 45
83 notation < "hvbox(a break maction (=) (=\sub t) b)"
84 non associative with precedence 45
85 for @{ 'eq $t $a $b }.
87 notation "hvbox(a break \leq b)"
88 non associative with precedence 45
91 notation "hvbox(a break \geq b)"
92 non associative with precedence 45
95 notation "hvbox(a break \lt b)"
96 non associative with precedence 45
99 notation "hvbox(a break \gt b)"
100 non associative with precedence 45
103 notation > "hvbox(a break \neq b)"
104 non associative with precedence 45
105 for @{ 'neq ? $a $b }.
107 notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
108 non associative with precedence 45
109 for @{ 'neq $t $a $b }.
111 notation "hvbox(a break \nleq b)"
112 non associative with precedence 45
113 for @{ 'nleq $a $b }.
115 notation "hvbox(a break \ngeq b)"
116 non associative with precedence 45
117 for @{ 'ngeq $a $b }.
119 notation "hvbox(a break \nless b)"
120 non associative with precedence 45
121 for @{ 'nless $a $b }.
123 notation "hvbox(a break \ngtr b)"
124 non associative with precedence 45
125 for @{ 'ngtr $a $b }.
127 notation "hvbox(a break \divides b)"
128 non associative with precedence 45
129 for @{ 'divides $a $b }.
131 notation "hvbox(a break \ndivides b)"
132 non associative with precedence 45
133 for @{ 'ndivides $a $b }.
135 notation "hvbox(a break + b)"
136 left associative with precedence 50
137 for @{ 'plus $a $b }.
139 notation "hvbox(a break - b)"
140 left associative with precedence 50
141 for @{ 'minus $a $b }.
143 notation "hvbox(a break * b)"
144 left associative with precedence 55
145 for @{ 'times $a $b }.
147 notation "hvbox(a break \middot b)"
148 left associative with precedence 55
149 for @{ 'middot $a $b }.
151 notation "hvbox(a break \mod b)"
152 left associative with precedence 55
153 for @{ 'module $a $b }.
156 non associative with precedence 90
157 for @{ 'divide $a $b }.
160 left associative with precedence 55
161 for @{ 'divide $a $b }.
163 notation "hvbox(a break / b)"
164 left associative with precedence 55
165 for @{ 'divide $a $b }.
167 notation "- term 60 a" with precedence 60
171 non associative with precedence 80
175 non associative with precedence 60
178 notation "hvbox(a break \lor b)"
179 left associative with precedence 30
182 notation "hvbox(a break \land b)"
183 left associative with precedence 35
186 notation "hvbox(\lnot a)"
187 non associative with precedence 40
190 notation > "hvbox(a break \liff b)"
191 left associative with precedence 25
194 notation "hvbox(a break \leftrightarrow b)"
195 left associative with precedence 25
199 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70
200 for @{ 'powerset $A }.
202 notation < "hvbox({ ident i | term 19 p })" with precedence 90
203 for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
205 notation > "hvbox({ ident i | term 19 p })" with precedence 90
206 for @{ 'subset (\lambda ${ident i}. $p)}.
208 notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
209 for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
211 notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
212 for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
214 notation "hvbox(a break ∈ b)" non associative with precedence 45
217 notation "hvbox(a break ≬ b)" non associative with precedence 45
218 for @{ 'overlaps $a $b }. (* \between *)
220 notation "hvbox(a break ⊆ b)" non associative with precedence 45
221 for @{ 'subseteq $a $b }. (* \subseteq *)
223 notation "hvbox(a break ∩ b)" non associative with precedence 55
224 for @{ 'intersects $a $b }. (* \cap *)
226 notation "hvbox(a break ∪ b)" non associative with precedence 50
227 for @{ 'union $a $b }. (* \cup *)
229 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
231 notation "hvbox(a break \approx b)" non associative with precedence 45
232 for @{ 'napart $a $b}.
234 notation "hvbox(a break # b)" non associative with precedence 45
235 for @{ 'apart $a $b}.
237 notation "hvbox(a break \circ b)"
238 left associative with precedence 55
239 for @{ 'compose $a $b }.
241 notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
242 notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
244 notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
246 notation "↑a" with precedence 55 for @{ 'uparrow $a }.
248 notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
250 notation "a \sup term 89 b" with precedence 90 for @{ 'exp $a $b}.
251 notation > "a ^ term 89 b" with precedence 90 for @{ 'exp $a $b}.
252 notation "s \sup (-1)" with precedence 90 for @{ 'invert $s }.
253 notation > "s ^ (-1)" with precedence 90 for @{ 'invert $s }.
254 notation < "s \sup (-1) x" with precedence 90 for @{ 'invert_appl $s $x}.
256 notation "hvbox(|term 90 C|)" with precedence 69 for @{ 'card $C }.
258 notation "\naturals" non associative with precedence 90 for @{'N}.
259 notation "\rationals" non associative with precedence 90 for @{'Q}.
260 notation "\reals" non associative with precedence 90 for @{'R}.
261 notation "\integers" non associative with precedence 90 for @{'Z}.
262 notation "\complexes" non associative with precedence 90 for @{'C}.
264 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
266 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
267 notation > "x ⊩_term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
268 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
269 notation > "⊩ " with precedence 60 for @{'Vdash ?}.
270 notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
272 notation < "maction (mstyle color #ff0000 (…)) (t)"
273 non associative with precedence 90 for @{'hide $t}.