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} : $ty. $p}
@{\lambda ${ident i} . $p}}}.
notation "hvbox(a break \to b)"
for @{ 'and $a $b }.
notation "hvbox(\lnot a)"
- left associative with precedence 40
+ non associative with precedence 40
for @{ 'not $a }.