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

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

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.6.0