Agda.Syntax.Fixity
Description
Definitions for fixity and precedence levels.
- data Fixity' = Fixity' {}
- type NewNotation = (Name, Fixity, Notation)
- oldToNewNotation :: (Name, Fixity') -> NewNotation
- syntaxOf :: Name -> Notation
- data Fixity
- fixityLevel :: Fixity -> Nat
- defaultFixity :: Fixity
- data Precedence
- 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'
The notation is handled as the fixity in the renamer. Hence they are grouped together in this type.
Constructors
Fixity' | |
Fields
|
type NewNotation = (Name, Fixity, Notation)
All the notation information related to a name.
oldToNewNotation :: (Name, Fixity') -> NewNotation
If an operator has no specific notation, recover it from its name.
data Fixity
Fixity of operators.
fixityLevel :: Fixity -> Nat
The default fixity. Currently defined to be
.
NonAssoc
20
data Precedence
Precedence is associated with a context.
Constructors
TopCtx | |
FunctionSpaceDomainCtx | |
LeftOperandCtx Fixity | |
RightOperandCtx Fixity | |
FunctionCtx | |
ArgumentCtx | |
InsideOperandCtx | |
WithFunCtx | |
WithArgCtx | |
DotPatternCtx |
Instances
hiddenArgumentCtx :: Hiding -> Precedence
The precedence corresponding to a possibly hidden argument.
opBrackets :: Fixity -> Precedence -> Bool
Do we need to bracket an operator application of the given fixity in a context with the given precedence.
lamBrackets :: Precedence -> Bool
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
Does a function application need brackets?
withAppBrackets :: Precedence -> Bool
Does a with application need brackets?
piBrackets :: Precedence -> Bool
Does a function space need brackets?
roundFixBrackets :: Precedence -> Bool