Agda.Syntax.Fixity

Notation coupled with Fixity

data Fixity'

data ThingWithFixity x

data NewNotation

namesToNotation

useDefaultFixity

notationNames

syntaxOf

noFixity'

mergeNotations

Sections

data NotationSection

noSection

Fixity

data PrecedenceLevel

data Associativity

data Fixity

noFixity

defaultFixity

Precendence

data Precedence

hiddenArgumentCtx

opBrackets

lamBrackets

appBrackets

withAppBrackets

piBrackets

roundFixBrackets

Some lenses

_notaFixity

_fixityAssoc

_fixityLevel

Printing

NFData instances