Agda-2.2.6: A dependently typed functional programming language and proof assistant



Definitions for fixity and precedence levels.



defaultFixity :: FixitySource

The default fixity. Currently defined to be LeftAssoc 20.

hiddenArgumentCtx :: Hiding -> PrecedenceSource

The precedence corresponding to a possibly hidden argument.

opBrackets :: Fixity -> Precedence -> BoolSource

Do we need to bracket an operator application of the given fixity in a context with the given precedence.

lamBrackets :: Precedence -> BoolSource

Does a lambda-like thing (lambda, let or pi) need brackets in the given context. A peculiar thing with lambdas is that they don't need brackets in a right operand context. For instance: m >>= x -> m' is a valid infix application.

appBrackets :: Precedence -> BoolSource

Does a function application need brackets?

withAppBrackets :: Precedence -> BoolSource

Does a with application need brackets?

piBrackets :: Precedence -> BoolSource

Does a function space need brackets?