Agda- A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered



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 = (Name, Fixity, Notation)Source

All the notation information related to a name.

oldToNewNotation :: (Name, 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?