Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




Definitions for fixity, precedence levels, and declared syntax.


Notation coupled with Fixity

data Fixity' Source

The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.



data NewNotation Source

All the notation information related to a name.




notaName :: QName
notaNames :: Set Name

The names the syntax and/or fixity belong to.

Invariant: The set is non-empty. Every name in the list matches notaName.

notaFixity :: Fixity

Associativity and precedence (fixity) of the names.

notation :: Notation

Syntax associated with the names.

namesToNotation :: QName -> Name -> NewNotation Source

If an operator has no specific notation, then it is computed from its name.

notationNames :: NewNotation -> [QName] Source

Return the IdParts of a notation, the first part qualified, the other parts unqualified. This allows for qualified use of operators, e.g., M.for x ∈ xs return e, or x ℕ.+ y.

syntaxOf :: Name -> Notation Source

Create a Notation (without binders) from a concrete Name. Does the obvious thing: Holes become NormalHoles, Ids become IdParts. If Name has no Holes, it returns noNotation.

mergeNotations :: [NewNotation] -> [NewNotation] Source

Merges all NewNotations that have the same notation.

If all NewNotations with a given notation have the same fixity, then this fixity is preserved, and otherwise it is replaced by defaultFixity.

Precondition: No Name may occur in more than one list element. Every NewNotation must have the same notaName.

Postcondition: No Name occurs in more than one list element.


defaultFixity :: Fixity Source

The default fixity. Currently defined to be NonAssoc 20.

noFixity :: Fixity Source

Hack used for syntax facility.


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 certain right operand contexts. However, we insert brackets anyway, for the following reasons:

  • Clarity.
  • Sometimes brackets are needed. Example: m₁ >>= (λ x → x) >>= m₂ (here _>>=_ is left associative).

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?