Agda-2.3.0.1: A dependently typed functional programming language and proof assistant

Agda.Syntax.Fixity

Description

Definitions for fixity and precedence levels.

Synopsis

# Documentation

data Fixity' Source

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

Constructors

 Fixity' FieldstheFixity :: Fixity theNotation :: Notation

Instances

 Eq Fixity' Data Fixity' Show Fixity' Typeable Fixity' EmbPrj Fixity'

Constructors

 ThingWithFixity x Fixity'

Instances

 Functor ThingWithFixity Typeable1 ThingWithFixity Foldable ThingWithFixity Traversable ThingWithFixity Data x => Data (ThingWithFixity x) Show x => Show (ThingWithFixity x) Pretty (ThingWithFixity Name) KillRange x => KillRange (ThingWithFixity x)

type NewNotation = (Name, Fixity, Notation)Source

All the notation information related to a name.

If an operator has no specific notation, recover it from its name.

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

The default fixity. Currently defined to be `NonAssoc 20`.

data Precedence Source

Precedence is associated with a context.

Instances

 Data Precedence Show Precedence Typeable Precedence EmbPrj Precedence

The precedence corresponding to a possibly hidden argument.

Do we need to bracket an operator application of the given fixity in a context with the given precedence.

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

Does a function application need brackets?

Does a with application need brackets?

Does a function space need brackets?