1 notation < "hvbox(\exists ident i opt (: ty) break . p)"
2 right associative with precedence 20
3 for @{ 'exists ${default
4 @{\lambda ${ident i} : $ty. $p}
5 @{\lambda ${ident i} . $p}}}.
7 notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
10 @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
11 @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
14 notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
15 right associative with precedence 20
16 for @{ 'sigma ${default
17 @{\lambda ${ident i} : $ty. $p}
18 @{\lambda ${ident i} . $p}}}.
20 notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
23 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
24 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
27 notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
28 with precedence 90 for @{ 'pair $a $b}.
30 notation "hvbox(x break \times y)" with precedence 70
31 for @{ 'product $x $y}.
33 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
34 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
36 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
37 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
39 notation > "\fst" with precedence 90 for @{'pi1}.
40 notation > "\snd" with precedence 90 for @{'pi2}.
42 notation "hvbox(a break \to b)"
43 right associative with precedence 20
44 for @{ \forall $_:$a.$b }.
46 notation < "hvbox(a break \to b)"
47 right associative with precedence 20
48 for @{ \Pi $_:$a.$b }.
50 notation "hvbox(a break = b)"
51 non associative with precedence 45
54 notation "hvbox(a break \leq b)"
55 non associative with precedence 45
58 notation "hvbox(a break \geq b)"
59 non associative with precedence 45
62 notation "hvbox(a break \lt b)"
63 non associative with precedence 45
66 notation "hvbox(a break \gt b)"
67 non associative with precedence 45
70 notation "hvbox(a break \neq b)"
71 non associative with precedence 45
74 notation "hvbox(a break \nleq b)"
75 non associative with precedence 45
78 notation "hvbox(a break \ngeq b)"
79 non associative with precedence 45
82 notation "hvbox(a break \nless b)"
83 non associative with precedence 45
84 for @{ 'nless $a $b }.
86 notation "hvbox(a break \ngtr b)"
87 non associative with precedence 45
90 notation "hvbox(a break \divides b)"
91 non associative with precedence 45
92 for @{ 'divides $a $b }.
94 notation "hvbox(a break \ndivides b)"
95 non associative with precedence 45
96 for @{ 'ndivides $a $b }.
98 notation "hvbox(a break + b)"
99 left associative with precedence 50
100 for @{ 'plus $a $b }.
102 notation "hvbox(a break - b)"
103 left associative with precedence 50
104 for @{ 'minus $a $b }.
106 notation "hvbox(a break * b)"
107 left associative with precedence 55
108 for @{ 'times $a $b }.
110 notation "hvbox(a break \middot b)"
111 left associative with precedence 55
112 for @{ 'middot $a $b }.
114 notation "hvbox(a break \mod b)"
115 left associative with precedence 55
116 for @{ 'module $a $b }.
119 non associative with precedence 90
120 for @{ 'divide $a $b }.
123 left associative with precedence 55
124 for @{ 'divide $a $b }.
126 notation "hvbox(a break / b)"
127 left associative with precedence 55
128 for @{ 'divide $a $b }.
130 notation "- term 60 a" with precedence 60
134 non associative with precedence 80
138 non associative with precedence 60
141 notation "hvbox(a break \lor b)"
142 left associative with precedence 30
145 notation "hvbox(a break \land b)"
146 left associative with precedence 35
149 notation "hvbox(\lnot a)"
150 non associative with precedence 40
153 notation > "hvbox(a break \liff b)"
154 left associative with precedence 25
157 notation "hvbox(a break \leftrightarrow b)"
158 left associative with precedence 25
162 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70
163 for @{ 'powerset $A }.
165 notation < "hvbox({ ident i | term 19 p })" with precedence 90
166 for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
168 notation > "hvbox({ ident i | term 19 p })" with precedence 90
169 for @{ 'subset (\lambda ${ident i}. $p)}.
171 notation "hvbox(a break ∈ b)" non associative with precedence 45
174 notation "hvbox(a break ≬ b)" non associative with precedence 45
175 for @{ 'overlaps $a $b }. (* \between *)
177 notation "hvbox(a break ⊆ b)" non associative with precedence 45
178 for @{ 'subseteq $a $b }. (* \subseteq *)
180 notation "hvbox(a break ∩ b)" non associative with precedence 55
181 for @{ 'intersects $a $b }. (* \cap *)
183 notation "hvbox(a break ∪ b)" non associative with precedence 50
184 for @{ 'union $a $b }. (* \cup *)
186 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
188 notation "hvbox(a break \approx b)" non associative with precedence 45
189 for @{ 'napart $a $b}.
191 notation "hvbox(a break # b)" non associative with precedence 45
192 for @{ 'apart $a $b}.
194 notation "hvbox(a break \circ b)"
195 left associative with precedence 55
196 for @{ 'compose $a $b }.
198 notation "(a \sup b)" left associative with precedence 60 for @{ 'exp $a $b}.
199 notation "s \sup (-1)" with precedence 60 for @{ 'invert $s }.
200 notation < "s \sup (-1) x" with precedence 60 for @{ 'invert_appl $s $x}.
202 notation "hvbox(|term 90 C|)" with precedence 69 for @{ 'card $C }.
204 notation "\naturals" non associative with precedence 90 for @{'N}.
205 notation "\rationals" non associative with precedence 90 for @{'Q}.
206 notation "\reals" non associative with precedence 90 for @{'R}.
207 notation "\integers" non associative with precedence 90 for @{'Z}.
208 notation "\complexes" non associative with precedence 90 for @{'C}.
210 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)