Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Fixity
Description
Definitions for fixity and precedence levels.
Synopsis
data Fixity' = Fixity' {
theFixity :: Fixity
theNotation :: Notation
}
type NewNotation = (Name, Fixity, Notation)
oldToNewNotation :: (Name, Fixity') -> NewNotation
syntaxOf :: Name -> Notation
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
The notation is handled as the fixity in the renamer. Hence they are grouped together in this type.
Constructors
Fixity'
theFixity :: Fixity
theNotation :: Notation
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.
syntaxOf :: Name -> NotationSource
data Fixity Source
Fixity of operators.
Constructors
LeftAssoc Range Nat
RightAssoc Range Nat
NonAssoc Range Nat
fixityLevel :: Fixity -> NatSource
defaultFixity :: FixitySource
The default fixity. Currently defined to be NonAssoc 20.
data Precedence Source
Precedence is associated with a context.
Constructors
TopCtx
FunctionSpaceDomainCtx
LeftOperandCtx Fixity
RightOperandCtx Fixity
FunctionCtx
ArgumentCtx
InsideOperandCtx
WithFunCtx
WithArgCtx
DotPatternCtx
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.6.1