Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Fixity
Description
Definitions for fixity and precedence levels.
Synopsis
data Fixity
= LeftAssoc Range Nat
| RightAssoc Range Nat
| NonAssoc Range Nat
fixityLevel :: Fixity -> Nat
defaultFixity :: Fixity
data Precedence
= TopCtx
| FunctionSpaceDomainCtx
| LeftOperandCtx Fixity
| RightOperandCtx Fixity
| FunctionCtx
| ArgumentCtx
| InsideOperandCtx
| WithFunCtx
| WithArgCtx
| DotPatternCtx
hiddenArgumentCtx :: Hiding -> Precedence
opBrackets :: Fixity -> Precedence -> Bool
lamBrackets :: Precedence -> Bool
appBrackets :: Precedence -> Bool
withAppBrackets :: Precedence -> Bool
piBrackets :: Precedence -> Bool
roundFixBrackets :: Precedence -> Bool
Documentation
data Fixity Source
Fixity of operators.
Constructors
LeftAssoc Range Nat
RightAssoc Range Nat
NonAssoc Range Nat
show/hide Instances
fixityLevel :: Fixity -> NatSource
defaultFixity :: FixitySource
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
show/hide Instances
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?
roundFixBrackets :: Precedence -> BoolSource
Produced by Haddock version 2.4.2