Lexical Structure

Agda code is written in UTF-8 encoded plain text files with the extension .agda; more file extensions are supported for Literate Programming. A UTF-8 byte order mark (BOM) is ignored at the beginning of a file.

Most unicode characters can be used in identifiers, see section Names. Whitespace is important, see section Layout.

Tokens

Keywords and special symbols

Most non-whitespace unicode can be used as part of an Agda name, but there are two kinds of exceptions:

special symbols

Characters with special meaning that cannot appear at all in a name. These are .;{}()@".

keywords

Reserved words that cannot appear as a name part, but can appear in a name together with other characters.

= | -> → : ? \ λ ∀ .. ... abstract coinductive constructor data do eta-equality field forall hiding import in inductive infix infixl infixr instance interleaved let macro module mutual no-eta-equality opaque open overlap pattern postulate primitive private public quote quoteTerm record renaming rewrite syntax tactic unfolding unquote unquoteDecl unquoteDef using variable where with

keywords in renaming directives

The word to is only reserved in renaming directives.

keywords in import statements

The word as has a special meaning in import statements, although it is not reserved.

Names

A qualified name is a non-empty sequence of names separated by dots (.). A name is an alternating sequence of name parts and underscores (_), containing at least one name part. A name part is a non-empty sequence of unicode characters, excluding whitespace, _, and special symbols. A name part cannot be one of the keywords above, and cannot start with a single quote, ' (which are used for character literals, see Literals below).

Examples

• Valid: data?, ::, if_then_else_, 0b, _⊢_∈_, x=y

• Invalid: data_?, foo__bar, _, a;b, [_.._]

The underscores in a name indicate where the arguments go when the name is used as an operator. For instance, the application _+_ 1 2 can be written as 1 + 2. See Mixfix Operators for more information. Since most sequences of characters are valid names, whitespace is more important than in other languages. In the example above the whitespace around + is required, since 1+2 is a valid name.

Qualified names are used to refer to entities defined in other modules. For instance Prelude.Bool.true refers to the name true defined in the module Prelude.Bool. See Module System for more information.

Literals

There are four types of literal values: integers, floats, characters, and strings. See Built-ins for the corresponding types, and Literal Overloading for how to support literals for user-defined types.

Integers

Integer values in decimal, hexadecimal (prefixed by 0x), or binary (prefixed by 0b) notation. The character _ can be used to separate groups of digits. Non-negative numbers map by default to built-in natural numbers, but can be overloaded. Negative numbers have no default interpretation and can only be used through overloading.

Examples: 123, 0xF0F080, -42, -0xF, 0b11001001, 1_000_000_000, 0b01001000_01001001.

Floats

Floating point numbers in the standard notation (with square brackets denoting optional parts):

float    ::= [-] decimal . decimal [exponent]
           | [-] decimal exponent
exponent ::= (e | E) [+ | -] decimal

These map to built-in floats and cannot be overloaded.

Examples: 1.0, -5.0e+12, 1.01e-16, 4.2E9, 50e3.

Characters

Character literals are enclosed in single quotes ('). They can be a single (unicode) character, other than ' or \, or an escaped character. Escaped characters start with a backslash \ followed by an escape code. Escape codes are natural numbers in decimal or hexadecimal (prefixed by x) between 0 and 0x10ffff (1114111), or one of the following special escape codes:

Character literals map to the built-in character type and cannot be overloaded.

Examples: 'A', '∀', '\x2200', '\ESC', '\32', '\n', '\'', '"'.

Strings

String literals are sequences of, possibly escaped, characters enclosed in double quotes ". They follow the same rules as character literals except that double quotes " need to be escaped rather than single quotes '. String literals map to the built-in string type by default, but can be overloaded.

Example: "Привет \"мир\"\n".

Holes

Holes are an integral part of the interactive development supported by the Emacs mode. Any text enclosed in {! and !} is a hole and may contain nested holes. A hole with no contents can be written ?. There are a number of Emacs commands that operate on the contents of a hole. The type checker ignores the contents of a hole and treats it as an unknown (see Implicit Arguments).

Example: {! f {!x!} 5 !}

Comments

Single-line comments are written with a double dash -- followed by arbitrary text. Multi-line comments are enclosed in {- and -} and can be nested. Comments cannot appear in string literals.

Example:

{- Here is a {- nested -}
   comment -}
s : String --line comment {-
s = "{- not a comment -}"

Pragmas

Pragmas are special comments enclosed in {-# and #-} that have special meaning to the system. See Pragmas for a full list of pragmas.

Layout

Agda is layout sensitive using similar rules as Haskell, with the exception that layout is mandatory: you cannot use explicit {, } and ; to avoid it.

A layout block contains a sequence of statements and is started by one of the layout keywords:

abstract
constructor
do
field
instance
let
macro
mutual
opaque
postulate
primitive
private
variable
where

The first token after the layout keyword decides the indentation of the block. Any token indented more than this is part of the previous statement, a token at the same level starts a new statement, and a token indented less lies outside the block.

data Nat : Set where -- starts a layout block
    -- comments are not tokens
  zero : Nat      -- statement 1
  suc  : Nat →    -- statement 2
         Nat      -- also statement 2
one : Nat -- outside the layout block
one = suc zero

Note that the indentation of the layout keyword does not matter.

If several layout blocks are started by layout keywords without line break in between (where line breaks inside block comments do not count), then those blocks indented more than the last block go passive, meaning they cannot be further extended by new statements:

private module M where postulate
          A : Set                 -- module-block goes passive
          B : Set                 -- postulate-block can still be extended
        module N where            -- private-block can still be extended

An Agda file contains one top-level layout block, with the special rule that the contents of the top-level module need not be indented.

module Example where
NotIndented : Set₁
NotIndented = Set

Literate Agda

Agda supports literate programming with multiple typesetting tools like LaTeX, Markdown and reStructuredText. For instance, with LaTeX, everything in a file is a comment unless enclosed in \begin{code}, \end{code}. Literate Agda files have special file extensions, like .lagda and .lagda.tex for LaTeX, .lagda.md for Markdown, .lagda.rst for reStructuredText instead of .agda. One use case for literate Agda files is to generate documents including Agda code. See Generating HTML and Generating LaTeX for more information.

\documentclass{article}
% some preamble stuff
\begin{document}
Introduction usually goes here
\begin{code}
module MyPaper where
  open import Prelude
  five : Nat
  five = 2 + 3
\end{code}
Now, conclusions!
\end{document}