Documentation

Fixity of operators.

Constructors

LeftAssoc Range Nat
RightAssoc Range Nat
NonAssoc Range Nat

Instances

Eq Fixity
Data Fixity
Show Fixity
Typeable Fixity
Pretty Fixity
HasRange Fixity
EmbPrj Fixity

fixityLevel :: Fixity -> Nat Source

defaultFixity :: Fixity Source

The default fixity. Currently defined to be LeftAssoc 20.

data Precedence Source

Precedence is associated with a context.

Constructors

TopCtx
FunctionSpaceDomainCtx
LeftOperandCtx Fixity
RightOperandCtx Fixity
FunctionCtx
ArgumentCtx
InsideOperandCtx
WithFunCtx
WithArgCtx
DotPatternCtx

Instances

Data Precedence
Show Precedence
Typeable Precedence
EmbPrj Precedence

hiddenArgumentCtx :: Hiding -> Precedence Source

The precedence corresponding to a possibly hidden argument.

opBrackets :: Fixity -> Precedence -> Bool Source

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

lamBrackets :: Precedence -> Bool Source

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 -> Bool Source

Does a function application need brackets?

withAppBrackets :: Precedence -> Bool Source

Does a with application need brackets?

piBrackets :: Precedence -> Bool Source

Does a function space need brackets?

roundFixBrackets :: Precedence -> Bool Source