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 \mod b)"
98 left associative with precedence 55
99 for @{ 'module $a $b }.
102 non associative with precedence 90
103 for @{ 'divide $a $b }.
106 left associative with precedence 55
107 for @{ 'divide $a $b }.
109 notation "hvbox(a break / b)"
110 left associative with precedence 55
111 for @{ 'divide $a $b }.
113 notation "- term 60 a" with precedence 60
117 non associative with precedence 80
120 notation "(a \sup b)"
121 right associative with precedence 65
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