+notation < "hvbox(\exists ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'exists ${default
+ @{\lambda ${ident i} : $ty. $p}
+ @{\lambda ${ident i} . $p}}}.
+
notation "hvbox(a break \to b)"
right associative with precedence 20
for @{ \forall $_:$a.$b }.
for @{ 'and $a $b }.
notation "hvbox(\lnot a)"
- left associative with precedence 40
+ non associative with precedence 40
for @{ 'not $a }.