| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 |

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

Produced by Haddock version 2.4.2