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(a break \to b)"
8 right associative with precedence 20
9 for @{ \forall $_:$a.$b }.
11 notation < "hvbox(a break \to b)"
12 right associative with precedence 20
13 for @{ \Pi $_:$a.$b }.
15 notation "hvbox(a break = b)"
16 non associative with precedence 45
19 notation "hvbox(a break \leq b)"
20 non associative with precedence 45
23 notation "hvbox(a break \geq b)"
24 non associative with precedence 45
27 notation "hvbox(a break \lt b)"
28 non associative with precedence 45
31 notation "hvbox(a break \gt b)"
32 non associative with precedence 45
35 notation "hvbox(a break \neq b)"
36 non associative with precedence 45
39 notation "hvbox(a break \nleq b)"
40 non associative with precedence 45
43 notation "hvbox(a break \ngeq b)"
44 non associative with precedence 45
47 notation "hvbox(a break \nless b)"
48 non associative with precedence 45
49 for @{ 'nless $a $b }.
51 notation "hvbox(a break \ngtr b)"
52 non associative with precedence 45
55 notation "hvbox(a break \divides b)"
56 non associative with precedence 45
57 for @{ 'divides $a $b }.
59 notation "hvbox(a break \ndivides b)"
60 non associative with precedence 45
61 for @{ 'ndivides $a $b }.
63 notation "hvbox(a break + b)"
64 left associative with precedence 50
67 notation "hvbox(a break - b)"
68 left associative with precedence 50
69 for @{ 'minus $a $b }.
71 notation "hvbox(a break * b)"
72 left associative with precedence 55
73 for @{ 'times $a $b }.
75 notation "hvbox(a break \mod b)"
76 left associative with precedence 55
77 for @{ 'module $a $b }.
80 non associative with precedence 90
81 for @{ 'divide $a $b }.
84 left associative with precedence 55
85 for @{ 'divide $a $b }.
87 notation "hvbox(a break / b)"
88 left associative with precedence 55
89 for @{ 'divide $a $b }.
91 notation "- term 60 a" with precedence 60
95 non associative with precedence 80
99 right associative with precedence 65
103 non associative with precedence 60
106 notation "hvbox(a break \lor b)"
107 left associative with precedence 30
110 notation "hvbox(a break \land b)"
111 left associative with precedence 35
114 notation "hvbox(\lnot a)"
115 non associative with precedence 40