• I do not want to type forall because it is too long, what can I do?
• How can I define a notation for square?
• Why don't "no associativity" and "left associativity" work at the same level?
• How can I know the associativity associated with a level?
• How to define a Haskell-like notation for list comprehension?