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




The concrete syntax is a raw representation of the program text without any desugaring at all. This is what the parser produces. The idea is that if we figure out how to keep the concrete syntax around, it can be printed exactly as the user wrote it.



data Expr Source

Concrete expressions. Should represent exactly what the user wrote.


Ident QName

ex: x

Lit Literal

ex: 1 or "foo"

QuestionMark !Range (Maybe Nat)

ex: ? or {! ... !}

Underscore !Range (Maybe Nat)

ex: _

RawApp !Range [Expr]

before parsing operators

App !Range Expr (NamedArg Expr)

ex: e e, e {e}, or e {x = e}

OpApp !Range Name [OpApp Expr]

ex: e + e

WithApp !Range Expr [Expr]

ex: e | e1 | .. | en

HiddenArg !Range (Named String Expr)

ex: {e} or {x=e}

InstanceArg !Range (Named String Expr)

ex: {{e}} or {{x=e}}

Lam !Range [LamBinding] Expr

ex: \x {y} -> e or \(x:A){y:B} -> e

AbsurdLam !Range Hiding

ex: \ ()

ExtendedLam !Range [(LHS, RHS, WhereClause)]

ex: \ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }

Fun !Range Expr Expr

ex: e -> e or .e -> e (NYI: {e} -> e)

Pi Telescope Expr

ex: (xs:e) -> e or {xs:e} -> e

Set !Range

ex: Set

Prop !Range

ex: Prop

SetN !Range Nat

ex: Set0, Set1, ..

Rec !Range [(Name, Expr)]

ex: record {x = a; y = b}

RecUpdate !Range Expr [(Name, Expr)]

ex: record e {x = a; y = b}

Let !Range [Declaration] Expr

ex: let Ds in e

Paren !Range Expr

ex: (e)

Absurd !Range

ex: () or {}, only in patterns

As !Range Name Expr

ex: x@p, only in patterns

Dot !Range Expr

ex: .p, only in patterns

ETel Telescope

only used for printing telescopes

QuoteGoal !Range Name Expr

ex: quoteGoal x in e

Quote !Range

ex: quote, should be applied to a name

QuoteTerm !Range

ex: quoteTerm, should be applied to a term

Unquote !Range

ex: unquote, should be applied to a term of type Term

DontCare Expr

to print irrelevant things

data OpApp e Source


SyntaxBindingLambda !Range [LamBinding] e

an abstraction inside a special syntax declaration (see Issue 358 why we introduce this).

Ordinary e 

fromOrdinary :: e -> OpApp e -> eSource

data AppView Source

The Expr is not an application.


AppView Expr [NamedArg Expr] 


data LamBinding Source

A lambda binding is either domain free or typed.


DomainFree Hiding Relevance BoundName

. x or {x} or .x or .{x} or {.x}

DomainFull TypedBindings

. (xs : e) or {xs : e}

data TypedBindings Source

A sequence of typed bindings with hiding information. Appears in dependent function spaces, typed lambdas, and telescopes.


TypedBindings !Range (Arg TypedBinding)

. (xs : e) or {xs : e}

type Telescope = [TypedBindings]Source

A telescope is a sequence of typed bindings. Bound variables are in scope in later types.


data Declaration Source

The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.


TypeSig Relevance Name Expr

Axioms and functions can be irrelevant.

Field Name (Arg Expr)

Record field, can be hidden and/or irrelevant.

FunClause LHS RHS WhereClause 
DataSig !Range Induction Name [LamBinding] Expr

lone data signature in mutual block

Data !Range Induction Name [LamBinding] (Maybe Expr) [Constructor] 
RecordSig !Range Name [LamBinding] Expr

lone record signature in mutual block

Record !Range Name (Maybe Name) [LamBinding] (Maybe Expr) [Declaration]

The optional name is a name for the record constructor.

Infix Fixity [Name] 
Syntax Name Notation

notation declaration for a name

Mutual !Range [Declaration] 
Abstract !Range [Declaration] 
Private !Range [Declaration] 
Postulate !Range [TypeSignature] 
Primitive !Range [TypeSignature] 
Open !Range QName ImportDirective 
Import !Range QName (Maybe AsName) OpenShortHand ImportDirective 
ModuleMacro !Range Name ModuleApplication OpenShortHand ImportDirective 
Module !Range QName [TypedBindings] [Declaration] 
Pragma Pragma 

type TypeSignature = DeclarationSource

Just type signatures.

type Constructor = TypeSignatureSource

A constructor or field declaration is just a type signature.

data ImportDirective Source

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).




importDirRange :: !Range
usingOrHiding :: UsingOrHiding
renaming :: [Renaming]
publicOpen :: Bool

Only for open. Exports the opened names from the current module.

data Renaming Source




renFrom :: ImportedName

Rename from this name.

renTo :: Name

To this one.

renToRange :: Range

The range of the "to" keyword. Retained for highlighting purposes.

data AsName Source




asName :: Name

The "as" name.

asRange :: Range

The range of the "as" keyword. Retained for highlighting purposes.

data LHS Source

Left hand sides can be written in infix style. For example:

 n + suc m = suc (n + m)
 (f  g) x = f (g x)

We use fixity information to see which name is actually defined.



original pattern, with-patterns, rewrite equations and with-expressions


lhsOriginalPattern :: Pattern
lhsWithPattern :: [Pattern]
lhsRewriteEqn :: [RewriteEqn]
lhsWithExpr :: [WithExpr]
Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]

new with-patterns, rewrite equations and with-expressions

type Module = ([Pragma], [Declaration])Source

Modules: Top-level pragmas plus other top-level declarations.

topLevelModuleName :: Module -> TopLevelModuleNameSource

Computes the top-level module name.

Precondition: The Module has to be well-formed.

Pattern tools

patternHead :: Pattern -> Maybe NameSource

Get the leftmost symbol in a pattern.

patternNames :: Pattern -> [Name]Source

Get all the identifiers in a pattern in left-to-right order.