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(\langle term 19 a, break term 19 b\rangle)"
139 with precedence 90 for @{ 'pair $a $b}.
141 notation "hvbox(x break \times y)" with precedence 70
142 for @{ 'product $x $y}.
144 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
145 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
147 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
148 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
150 notation > "\fst" with precedence 90 for @{'pi1}.
151 notation > "\snd" with precedence 90 for @{'pi2}.
154 notation "hvbox(a break \to b)"
155 right associative with precedence 20
156 for @{ \forall $_:$a.$b }.
158 notation < "hvbox(a break \to b)"
159 right associative with precedence 20
160 for @{ \Pi $_:$a.$b }.
163 notation "hvbox(a break \leq b)"
164 non associative with precedence 45
167 notation "hvbox(a break \geq b)"
168 non associative with precedence 45
171 notation "hvbox(a break \lt b)"
172 non associative with precedence 45
175 notation "hvbox(a break \gt b)"
176 non associative with precedence 45
179 notation > "hvbox(a break \neq b)"
180 non associative with precedence 45
181 for @{ 'neq ? $a $b }.
183 notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
184 non associative with precedence 45
185 for @{ 'neq $t $a $b }.
187 notation "hvbox(a break \nleq b)"
188 non associative with precedence 45
189 for @{ 'nleq $a $b }.
191 notation "hvbox(a break \ngeq b)"
192 non associative with precedence 45
193 for @{ 'ngeq $a $b }.
195 notation "hvbox(a break \nless b)"
196 non associative with precedence 45
197 for @{ 'nless $a $b }.
199 notation "hvbox(a break \ngtr b)"
200 non associative with precedence 45
201 for @{ 'ngtr $a $b }.
203 notation "hvbox(a break \divides b)"
204 non associative with precedence 45
205 for @{ 'divides $a $b }.
207 notation "hvbox(a break \ndivides b)"
208 non associative with precedence 45
209 for @{ 'ndivides $a $b }.
211 notation "hvbox(a break + b)"
212 left associative with precedence 55
213 for @{ 'plus $a $b }.
215 notation "hvbox(a break - b)"
216 left associative with precedence 55
217 for @{ 'minus $a $b }.
219 notation "hvbox(a break * b)"
220 left associative with precedence 60
221 for @{ 'times $a $b }.
223 notation "hvbox(a break \middot b)"
224 left associative with precedence 60
225 for @{ 'middot $a $b }.
227 notation "hvbox(a break \mod b)"
228 left associative with precedence 60
229 for @{ 'module $a $b }.
231 notation < "a \frac b"
232 non associative with precedence 90
233 for @{ 'divide $a $b }.
236 left associative with precedence 60
237 for @{ 'divide $a $b }.
239 notation "hvbox(a break / b)"
240 left associative with precedence 60
241 for @{ 'divide $a $b }.
243 notation "- term 65 a" with precedence 65
247 non associative with precedence 65
250 notation "hvbox(a break \lor b)"
251 left associative with precedence 30
254 notation "hvbox(a break \land b)"
255 left associative with precedence 35
258 notation "hvbox(\lnot a)"
259 non associative with precedence 40
262 notation > "hvbox(a break \liff b)"
263 left associative with precedence 25
266 notation "hvbox(a break \leftrightarrow b)"
267 left associative with precedence 25
271 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
272 for @{ 'powerset $A }.
273 notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
274 for @{ 'powerset $A }.
276 notation "hvbox(a break ∈ b)" non associative with precedence 45
279 notation "hvbox(a break ∉ b)" non associative with precedence 45
280 for @{ 'notmem $a $b }.
282 notation "hvbox(a break ≬ b)" non associative with precedence 45
283 for @{ 'overlaps $a $b }. (* \between *)
285 notation "hvbox(a break ⊆ b)" non associative with precedence 45
286 for @{ 'subseteq $a $b }. (* \subseteq *)
288 notation "hvbox(a break ∩ b)" left associative with precedence 60
289 for @{ 'intersects $a $b }. (* \cap *)
291 notation "hvbox(a break ∪ b)" left associative with precedence 55
292 for @{ 'union $a $b }. (* \cup *)
294 notation "hvbox(a break \approx b)" non associative with precedence 45
295 for @{ 'napart $a $b}.
297 notation "hvbox(a break # b)" non associative with precedence 45
298 for @{ 'apart $a $b}.
300 notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
301 notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
302 notation > "a ^ term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
304 notation "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
306 notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}.
308 notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
310 notation "\naturals" non associative with precedence 90 for @{'N}.
311 notation "\rationals" non associative with precedence 90 for @{'Q}.
312 notation "\reals" non associative with precedence 90 for @{'R}.
313 notation "\integers" non associative with precedence 90 for @{'Z}.
314 notation "\complexes" non associative with precedence 90 for @{'C}.
316 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
318 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
319 notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
320 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
321 notation > "⊩ " with precedence 65 for @{'Vdash ?}.
322 notation "(⊩ \sub term 90 c) " with precedence 65 for @{'Vdash $c}.
324 notation < "maction (mstyle color #ff0000 (…)) (t)"
325 non associative with precedence 90 for @{'hide $t}.