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

Agda.Syntax.Fixity

Description

Definitions for fixity and precedence levels.

Synopsis

Documentation

data Fixity' Source

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

Constructors

Fixity' 

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 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?