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(x break \times y)" with precedence 70
115 for @{ 'product $x $y}.
117 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
118 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
120 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
121 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
123 notation > "\fst" with precedence 90 for @{'pi1}.
124 notation > "\snd" with precedence 90 for @{'pi2}.
126 (* implication **************************************************************)
128 notation "hvbox(a break \to b)"
129 right associative with precedence 20
130 for @{ \forall $_:$a.$b }.
132 notation < "hvbox(a break \to b)"
133 right associative with precedence 20
134 for @{ \Pi $_:$a.$b }.
136 (* orders *******************************************************************)
138 notation "hvbox(a break \leq b)"
139 non associative with precedence 45
142 notation "hvbox(a break \geq b)"
143 non associative with precedence 45
146 notation "hvbox(a break \lt b)"
147 non associative with precedence 45
150 notation "hvbox(a break \gt b)"
151 non associative with precedence 45
154 (* negated equality *********************************************************)
156 notation > "hvbox(a break \neq b)"
157 non associative with precedence 45
158 for @{ 'neq ? $a $b }.
160 notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
161 non associative with precedence 45
162 for @{ 'neq $t $a $b }.
164 (* negated orders ***********************************************************)
166 notation "hvbox(a break \nleq b)"
167 non associative with precedence 45
168 for @{ 'nleq $a $b }.
170 notation "hvbox(a break \ngeq b)"
171 non associative with precedence 45
172 for @{ 'ngeq $a $b }.
174 notation "hvbox(a break \nless b)"
175 non associative with precedence 45
176 for @{ 'nless $a $b }.
178 notation "hvbox(a break \ngtr b)"
179 non associative with precedence 45
180 for @{ 'ngtr $a $b }.
182 (* divides, negated divides *************************************************)
184 notation "hvbox(a break \divides b)"
185 non associative with precedence 45
186 for @{ 'divides $a $b }.
188 notation "hvbox(a break \ndivides b)"
189 non associative with precedence 45
190 for @{ 'ndivides $a $b }.
192 (* arithmetics **************************************************************)
194 notation "hvbox(a break + b)"
195 left associative with precedence 55
196 for @{ 'plus $a $b }.
198 notation "hvbox(a break - b)"
199 left associative with precedence 55
200 for @{ 'minus $a $b }.
202 notation "hvbox(a break * b)"
203 left associative with precedence 60
204 for @{ 'times $a $b }.
206 notation "hvbox(a break \middot b)"
207 left associative with precedence 60
208 for @{ 'middot $a $b }.
210 notation "hvbox(a break \mod b)"
211 left associative with precedence 60
212 for @{ 'module $a $b }.
214 notation < "a \frac b"
215 non associative with precedence 90
216 for @{ 'divide $a $b }.
219 left associative with precedence 60
220 for @{ 'divide $a $b }.
222 notation "hvbox(a break / b)"
223 left associative with precedence 60
224 for @{ 'divide $a $b }.
226 notation "- term 65 a" with precedence 65
230 non associative with precedence 65
233 (* logical connectives ******************************************************)
235 notation "hvbox(a break \lor b)"
236 left associative with precedence 30
239 notation "hvbox(a break \land b)"
240 left associative with precedence 35
243 notation "hvbox(\lnot a)"
244 non associative with precedence 40
247 notation > "hvbox(a break \liff b)"
248 left associative with precedence 25
251 notation "hvbox(a break \leftrightarrow b)"
252 left associative with precedence 25
255 (* subsets ******************************************************************)
257 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
258 for @{ 'powerset $A }.
260 notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
261 for @{ 'powerset $A }.
263 notation "hvbox(a break ∈ b)" non associative with precedence 45
266 notation "hvbox(a break ∉ b)" non associative with precedence 45
267 for @{ 'notmem $a $b }.
269 notation "hvbox(a break ∩ b)" left associative with precedence 60
270 for @{ 'intersects $a $b }. (* \cap *)
272 notation "hvbox(a break ∪ b)" left associative with precedence 55
273 for @{ 'union $a $b }. (* \cup *)
275 (* other notations **********************************************************)
277 notation "\naturals" non associative with precedence 90 for @{'N}.
278 notation "\rationals" non associative with precedence 90 for @{'Q}.
279 notation "\reals" non associative with precedence 90 for @{'R}.
280 notation "\integers" non associative with precedence 90 for @{'Z}.
281 notation "\complexes" non associative with precedence 90 for @{'C}.
283 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
285 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
286 notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
287 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
288 notation > "⊩ " with precedence 65 for @{'Vdash ?}.
289 notation "(⊩ \sub term 90 c) " with precedence 65 for @{'Vdash $c}.
291 notation < "maction (mstyle color #ff0000 (…)) (t)"
292 non associative with precedence 90 for @{'hide $t}.