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(\langle term 19 a, break term 19 b\rangle)"
15 with precedence 90 for @{ 'pair $a $b}.
17 notation "hvbox(x break \times y)" with precedence 70
18 for @{ 'product $x $y}.
20 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
21 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
23 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
24 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
26 notation > "\fst" with precedence 90 for @{'pi1}.
27 notation > "\snd" with precedence 90 for @{'pi2}.
29 notation "hvbox(a break \to b)"
30 right associative with precedence 20
31 for @{ \forall $_:$a.$b }.
33 notation < "hvbox(a break \to b)"
34 right associative with precedence 20
35 for @{ \Pi $_:$a.$b }.
37 notation "hvbox(a break = b)"
38 non associative with precedence 45
41 notation "hvbox(a break \leq b)"
42 non associative with precedence 45
45 notation "hvbox(a break \geq b)"
46 non associative with precedence 45
49 notation "hvbox(a break \lt b)"
50 non associative with precedence 45
53 notation "hvbox(a break \gt b)"
54 non associative with precedence 45
57 notation "hvbox(a break \neq b)"
58 non associative with precedence 45
61 notation "hvbox(a break \nleq b)"
62 non associative with precedence 45
65 notation "hvbox(a break \ngeq b)"
66 non associative with precedence 45
69 notation "hvbox(a break \nless b)"
70 non associative with precedence 45
71 for @{ 'nless $a $b }.
73 notation "hvbox(a break \ngtr b)"
74 non associative with precedence 45
77 notation "hvbox(a break \divides b)"
78 non associative with precedence 45
79 for @{ 'divides $a $b }.
81 notation "hvbox(a break \ndivides b)"
82 non associative with precedence 45
83 for @{ 'ndivides $a $b }.
85 notation "hvbox(a break + b)"
86 left associative with precedence 50
89 notation "hvbox(a break - b)"
90 left associative with precedence 50
91 for @{ 'minus $a $b }.
93 notation "hvbox(a break * b)"
94 left associative with precedence 55
95 for @{ 'times $a $b }.
97 notation "hvbox(a break \middot b)"
98 left associative with precedence 55
99 for @{ 'middot $a $b }.
101 notation "hvbox(a break \mod b)"
102 left associative with precedence 55
103 for @{ 'module $a $b }.
106 non associative with precedence 90
107 for @{ 'divide $a $b }.
110 left associative with precedence 55
111 for @{ 'divide $a $b }.
113 notation "hvbox(a break / b)"
114 left associative with precedence 55
115 for @{ 'divide $a $b }.
117 notation "- term 60 a" with precedence 60
121 non associative with precedence 80
125 non associative with precedence 60
128 notation "hvbox(a break \lor b)"
129 left associative with precedence 30
132 notation "hvbox(a break \land b)"
133 left associative with precedence 35
136 notation "hvbox(\lnot a)"
137 non associative with precedence 40
140 notation > "hvbox(a break \liff b)"
141 left associative with precedence 25
144 notation "hvbox(a break \leftrightarrow b)"
145 left associative with precedence 25
149 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70
150 for @{ 'powerset $A }.
152 notation < "hvbox({ ident i | term 19 p })" with precedence 90
153 for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
155 notation > "hvbox({ ident i | term 19 p })" with precedence 90
156 for @{ 'subset (\lambda ${ident i}. $p)}.
158 notation "hvbox(a break ∈ b)" non associative with precedence 45
161 notation "hvbox(a break ≬ b)" non associative with precedence 45
162 for @{ 'overlaps $a $b }. (* \between *)
164 notation "hvbox(a break ⊆ b)" non associative with precedence 45
165 for @{ 'subseteq $a $b }. (* \subseteq *)
167 notation "hvbox(a break ∩ b)" non associative with precedence 55
168 for @{ 'intersects $a $b }. (* \cap *)
170 notation "hvbox(a break ∪ b)" non associative with precedence 50
171 for @{ 'union $a $b }. (* \cup *)
173 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
175 notation "hvbox(a break \approx b)" non associative with precedence 45
176 for @{ 'napart $a $b}.
178 notation "hvbox(a break # b)" non associative with precedence 45
179 for @{ 'apart $a $b}.
181 notation "hvbox(a break \circ b)"
182 left associative with precedence 55
183 for @{ 'compose $a $b }.
185 notation "(a \sup b)" left associative with precedence 60 for @{ 'exp $a $b}.
186 notation "s \sup (-1)" with precedence 60 for @{ 'invert $s }.
187 notation < "s \sup (-1) x" with precedence 60 for @{ 'invert_appl $s $x}.
190 notation "\naturals" non associative with precedence 90 for @{'N}.
191 notation "\rationals" non associative with precedence 90 for @{'Q}.
192 notation "\reals" non associative with precedence 90 for @{'R}.
193 notation "\integers" non associative with precedence 90 for @{'Z}.
194 notation "\complexes" non associative with precedence 90 for @{'C}.
196 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)