1 notation "1" with precedence 90 for @{'idpath}.
3 notation < "hvbox(l1 break # _(term 90 F) (term 47 l2))"
4 non associative with precedence 47
5 for @{'transport $F $l1 $l2 }.
7 notation > "hvbox(l1 break # l2)"
8 right associative with precedence 47
9 for @{'transport ? $l1 $l2 }.
11 notation "hvbox(l1 break @ l2)"
12 right associative with precedence 49
13 for @{'append $l1 $l2 }.
15 (* exists *******************************************************************)
17 notation "hvbox(∃ _ break . p)"
21 notation < "hvbox(\exists ident i : ty break . p)"
22 right associative with precedence 20
23 for @{'exists (\lambda ${ident i} : $ty. $p) }.
25 notation < "hvbox(\exists ident i break . p)"
27 for @{'exists (\lambda ${ident i}. $p) }.
29 notation "hvbox(〈term 19 a, break term 19 b〉)"
30 with precedence 90 for @{ 'mk_exists $a $b }.
33 notation < "hvbox(\exists ident i opt (: ty) break . p)"
34 right associative with precedence 20
35 for @{ 'exists ${default
36 @{\lambda ${ident i} : $ty. $p}
37 @{\lambda ${ident i} . $p}}}.
40 notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
43 @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
44 @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
48 notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
49 non associative with precedence 20
50 for @{ 'exists2 (λ${ident x0}.$P0) (λ${ident x0}.$P1) }.
52 notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
53 non associative with precedence 20
54 for @{ 'exists2 (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) }.
56 (* sigma ********************************************************************)
58 notation < "hvbox(\Sigma ident i : ty break . p)"
59 left associative with precedence 20
60 for @{'sigma (\lambda ${ident i} : $ty. $p) }.
62 notation < "hvbox(\Sigma ident i break . p)"
64 for @{'sigma (\lambda ${ident i}. $p) }.
67 notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
68 right associative with precedence 20
69 for @{ 'sigma ${default
70 @{\lambda ${ident i} : $ty. $p}
71 @{\lambda ${ident i} . $p}}}.
74 notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
77 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
78 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
81 notation "hvbox(« term 19 a, break term 19 b»)"
82 with precedence 90 for @{ 'dp $a $b }.
84 (* dependent pairs (i.e. Sigma with predicate in Type[0]) ********************)
86 notation < "hvbox(𝚺 ident i : ty break . p)"
87 left associative with precedence 20
88 for @{'dpair (\lambda ${ident i} : $ty. $p) }.
90 notation < "hvbox(𝚺 ident i break . p)"
92 for @{'dpair (\lambda ${ident i}. $p) }.
95 notation < "hvbox(𝚺 ident i opt (: ty) break . p)"
96 right associative with precedence 20
97 for @{ 'dpair ${default
98 @{\lambda ${ident i} : $ty. $p}
99 @{\lambda ${ident i} . $p}}}.
102 notation > "𝚺 list1 ident x sep , opt (: T). term 19 Px"
105 @{ ${ fold right @{$Px} rec acc @{'dpair (λ${ident x}:$T.$acc)} } }
106 @{ ${ fold right @{$Px} rec acc @{'dpair (λ${ident x}.$acc)} } }
109 notation "hvbox(❬ term 19 a, break term 19 b❭)"
110 with precedence 90 for @{ 'mk_DPair $a $b }.
113 (* equality, conguence ******************************************************)
115 notation > "hvbox(a break = b)"
116 non associative with precedence 45
117 for @{ 'eq ? $a $b }.
119 notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)"
120 non associative with precedence 45
121 for @{ 'eq $t $a $b }.
123 notation > "hvbox(n break ≅ m)"
124 non associative with precedence 45
125 for @{ 'congruent $n $m ? }.
127 notation < "hvbox(term 46 n break ≅ _ term 90 p term 46 m)"
128 non associative with precedence 45
129 for @{ 'congruent $n $m $p }.
131 notation "hvbox(n break ≡ m)"
132 non associative with precedence 45
133 for @{ 'equiv $n $m }.
136 (* other notations **********************************************************)
138 notation "hvbox(x break \times y)" with precedence 70
139 for @{ 'product $x $y}.
141 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
142 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
144 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
145 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
147 notation > "\fst" with precedence 90 for @{'pi1}.
148 notation > "\snd" with precedence 90 for @{'pi2}.
151 notation "hvbox(a break \to b)"
152 right associative with precedence 20
153 for @{ \forall $_:$a.$b }.
155 notation < "hvbox(a break \to b)"
156 right associative with precedence 20
157 for @{ \Pi $_:$a.$b }.
160 notation "hvbox(a break \leq b)"
161 non associative with precedence 45
164 notation "hvbox(a break \geq b)"
165 non associative with precedence 45
168 notation "hvbox(a break \lt b)"
169 non associative with precedence 45
172 notation "hvbox(a break \gt b)"
173 non associative with precedence 45
176 notation > "hvbox(a break \neq b)"
177 non associative with precedence 45
178 for @{ 'neq ? $a $b }.
180 notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
181 non associative with precedence 45
182 for @{ 'neq $t $a $b }.
184 notation "hvbox(a break \nleq b)"
185 non associative with precedence 45
186 for @{ 'nleq $a $b }.
188 notation "hvbox(a break \ngeq b)"
189 non associative with precedence 45
190 for @{ 'ngeq $a $b }.
192 notation "hvbox(a break \nless b)"
193 non associative with precedence 45
194 for @{ 'nless $a $b }.
196 notation "hvbox(a break \ngtr b)"
197 non associative with precedence 45
198 for @{ 'ngtr $a $b }.
200 notation "hvbox(a break \divides b)"
201 non associative with precedence 45
202 for @{ 'divides $a $b }.
204 notation "hvbox(a break \ndivides b)"
205 non associative with precedence 45
206 for @{ 'ndivides $a $b }.
208 notation "hvbox(a break + b)"
209 left associative with precedence 55
210 for @{ 'plus $a $b }.
212 notation "hvbox(a break - b)"
213 left associative with precedence 55
214 for @{ 'minus $a $b }.
216 notation "hvbox(a break * b)"
217 left associative with precedence 60
218 for @{ 'times $a $b }.
220 notation "hvbox(a break \middot b)"
221 left associative with precedence 60
222 for @{ 'middot $a $b }.
224 notation "hvbox(a break \mod b)"
225 left associative with precedence 60
226 for @{ 'module $a $b }.
228 notation < "a \frac b"
229 non associative with precedence 90
230 for @{ 'divide $a $b }.
233 left associative with precedence 60
234 for @{ 'divide $a $b }.
236 notation "hvbox(a break / b)"
237 left associative with precedence 60
238 for @{ 'divide $a $b }.
240 notation "- term 65 a" with precedence 65
244 non associative with precedence 65
247 notation "hvbox(a break \lor b)"
248 left associative with precedence 30
251 notation "hvbox(a break \land b)"
252 left associative with precedence 35
255 notation "hvbox(\lnot a)"
256 non associative with precedence 40
259 notation > "hvbox(a break \liff b)"
260 left associative with precedence 25
263 notation "hvbox(a break \leftrightarrow b)"
264 left associative with precedence 25
268 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
269 for @{ 'powerset $A }.
270 notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
271 for @{ 'powerset $A }.
273 notation "hvbox(a break ∈ b)" non associative with precedence 45
276 notation "hvbox(a break ∉ b)" non associative with precedence 45
277 for @{ 'notmem $a $b }.
279 notation "hvbox(a break ≬ b)" non associative with precedence 45
280 for @{ 'overlaps $a $b }. (* \between *)
282 notation "hvbox(a break ⊆ b)" non associative with precedence 45
283 for @{ 'subseteq $a $b }. (* \subseteq *)
285 notation "hvbox(a break ∩ b)" left associative with precedence 60
286 for @{ 'intersects $a $b }. (* \cap *)
288 notation "hvbox(a break ∪ b)" left associative with precedence 55
289 for @{ 'union $a $b }. (* \cup *)
291 notation "hvbox(a break \approx b)" non associative with precedence 45
292 for @{ 'napart $a $b}.
294 notation "hvbox(a break # b)" non associative with precedence 45
295 for @{ 'apart $a $b}.
297 notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
298 notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
299 notation > "a ^ term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
301 notation "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
303 notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}.
305 notation "\naturals" non associative with precedence 90 for @{'N}.
306 notation "\rationals" non associative with precedence 90 for @{'Q}.
307 notation "\reals" non associative with precedence 90 for @{'R}.
308 notation "\integers" non associative with precedence 90 for @{'Z}.
309 notation "\complexes" non associative with precedence 90 for @{'C}.
311 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
313 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
314 notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
315 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
316 notation > "⊩ " with precedence 65 for @{'Vdash ?}.
317 notation "(⊩ \sub term 90 c) " with precedence 65 for @{'Vdash $c}.
319 notation < "maction (mstyle color #ff0000 (…)) (t)"
320 non associative with precedence 90 for @{'hide $t}.