Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



Definitions for fixity and precedence levels.



data Fixity' Source

The notation is handled as the fixity in the renamer. Hence they are grouped together in this type.



type NewNotation = (QName, Fixity, Notation)Source

All the notation information related to a name.

oldToNewNotation :: (QName, Fixity') -> NewNotationSource

If an operator has no specific notation, recover it from its name.

defaultFixity :: FixitySource

The default fixity. Currently defined to be NonAssoc 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 certain right operand contexts. However, we insert brackets anyway, for the following reasons:

  • Clarity.
  • Sometimes brackets are needed. Example: m₁ >>= (λ x → x) >>= m₂ (here _>>=_ is left associative).

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?