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 "hvbox(\langle term 19 a, break term 19 b\rangle)"
8 with precedence 90 for @{ 'pair $a $b}.
10 notation "hvbox(x break \times y)" with precedence 70
11 for @{ 'product $x $y}.
13 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
14 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
16 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
17 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
19 notation > "\fst" with precedence 90 for @{'pi1}.
20 notation > "\snd" with precedence 90 for @{'pi2}.
22 notation "hvbox(a break \to b)"
23 right associative with precedence 20
24 for @{ \forall $_:$a.$b }.
26 notation < "hvbox(a break \to b)"
27 right associative with precedence 20
28 for @{ \Pi $_:$a.$b }.
30 notation "hvbox(a break = b)"
31 non associative with precedence 45
34 notation "hvbox(a break \leq b)"
35 non associative with precedence 45
38 notation "hvbox(a break \geq b)"
39 non associative with precedence 45
42 notation "hvbox(a break \lt b)"
43 non associative with precedence 45
46 notation "hvbox(a break \gt b)"
47 non associative with precedence 45
50 notation "hvbox(a break \neq b)"
51 non associative with precedence 45
54 notation "hvbox(a break \nleq b)"
55 non associative with precedence 45
58 notation "hvbox(a break \ngeq b)"
59 non associative with precedence 45
62 notation "hvbox(a break \nless b)"
63 non associative with precedence 45
64 for @{ 'nless $a $b }.
66 notation "hvbox(a break \ngtr b)"
67 non associative with precedence 45
70 notation "hvbox(a break \divides b)"
71 non associative with precedence 45
72 for @{ 'divides $a $b }.
74 notation "hvbox(a break \ndivides b)"
75 non associative with precedence 45
76 for @{ 'ndivides $a $b }.
78 notation "hvbox(a break + b)"
79 left associative with precedence 50
82 notation "hvbox(a break - b)"
83 left associative with precedence 50
84 for @{ 'minus $a $b }.
86 notation "hvbox(a break * b)"
87 left associative with precedence 55
88 for @{ 'times $a $b }.
90 notation "hvbox(a break \mod b)"
91 left associative with precedence 55
92 for @{ 'module $a $b }.
95 non associative with precedence 90
96 for @{ 'divide $a $b }.
99 left associative with precedence 55
100 for @{ 'divide $a $b }.
102 notation "hvbox(a break / b)"
103 left associative with precedence 55
104 for @{ 'divide $a $b }.
106 notation "- term 60 a" with precedence 60
110 non associative with precedence 80
113 notation "(a \sup b)"
114 right associative with precedence 65
118 non associative with precedence 60
121 notation "hvbox(a break \lor b)"
122 left associative with precedence 30
125 notation "hvbox(a break \land b)"
126 left associative with precedence 35
129 notation "hvbox(\lnot a)"
130 non associative with precedence 40