Here is a way of defining precedence that is quite general: https://obua.com/publications/practical-types/1/ https://obua.com/publications/practical-types/1/ (

Here is a way of defining precedence that is quite general: https://obua.com/publications/practical-types/1/ https://obua.com/publications/practical-types/1/ (Search for APP_PRIO in the document to get to where this is talked about) Basically, an expression "A + B" is given a certain precedence, and both A and B are expected to have higher precedence. You can modify that by putting a ` in front of any nonterminal, for example "`A + B", which means that A can have indeed the same precedence as "A + B". This way you can specify associativity, and this works also in other cases, for example "∀ x. `P" means that something like "∀ x. ∀ y. x = y" parses correctly instead of having to write "∀ x. (∀ y. x = y)"