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 65
236 (* logical connectives ******************************************************)
238 notation "hvbox(a break \lor b)"
239 left associative with precedence 30
242 notation "hvbox(a break \land b)"
243 left associative with precedence 35
246 notation "hvbox(\lnot a)"
247 non associative with precedence 40
250 notation > "hvbox(a break \liff b)"
251 left associative with precedence 25
254 notation "hvbox(a break \leftrightarrow b)"
255 left associative with precedence 25
258 (* subsets ******************************************************************)
260 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
261 for @{ 'powerset $A }.
263 notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
264 for @{ 'powerset $A }.
266 notation "hvbox(a break ∈ b)" non associative with precedence 45
269 notation "hvbox(a break ∉ b)" non associative with precedence 45
270 for @{ 'notmem $a $b }.
272 notation "hvbox(a break ≬ b)" non associative with precedence 45
273 for @{ 'overlaps $a $b }. (* \between *)
275 notation "hvbox(a break ∩ b)" left associative with precedence 60
276 for @{ 'intersects $a $b }. (* \cap *)
278 notation "hvbox(a break ∪ b)" left associative with precedence 55
279 for @{ 'union $a $b }. (* \cup *)
281 (* other notations **********************************************************)
283 notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
284 notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
285 notation > "a ^ term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
286 notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }.
287 notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
288 notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}.
290 notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
292 notation "\naturals" non associative with precedence 90 for @{'N}.
293 notation "\rationals" non associative with precedence 90 for @{'Q}.
294 notation "\reals" non associative with precedence 90 for @{'R}.
295 notation "\integers" non associative with precedence 90 for @{'Z}.
296 notation "\complexes" non associative with precedence 90 for @{'C}.
298 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
300 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
301 notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
302 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
303 notation > "⊩ " with precedence 65 for @{'Vdash ?}.
304 notation "(⊩ \sub term 90 c) " with precedence 65 for @{'Vdash $c}.
306 notation < "maction (mstyle color #ff0000 (…)) (t)"
307 non associative with precedence 90 for @{'hide $t}.