Emacs Mode

Agda programs can be edited in Emacs with support by the agda-mode, which is maintained by the Agda developers in the main Agda repository and offers many advanced features. To use it, first ensure you have installed Agda, installed Emacs, and installed agda-mode.

To edit a module in Emacs, open a file ending in .agda and load it by pressing C-c C-l (other commands are listed under Notation for key combinations below). This will apply syntax highlighting to the code and display any errors in a separate buffer. Agda uses certain background colors to indicate specific issues with the code, see Background highlighting below.

Installation

After installing the agda program and Emacs, run the following command:

agda --emacs-mode setup

The above command will first write the Agda data files to the Agda data directory (see --print-agda-data-dir) if this directory does not exist yet. (To force writing the data files there use the --setup option of agda.)

It then tries to set up Emacs for use with Agda. As an alternative you can copy the following text to your .emacs file:

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda --emacs-mode locate")))

It is also possible (but not necessary) to compile the Emacs mode’s files:

agda --emacs-mode compile

This can, in some cases, give a noticeable speedup.

Warning

If you reinstall the Agda mode without recompiling the Emacs Lisp files, then Emacs may continue using the old, compiled files.

Configuration

If you want to you can customise the Emacs mode. Just start Emacs and type the following:

M-x load-library RET agda2-mode RET
M-x customize-group RET agda2 RET

If you want some specific settings for the Emacs mode you can add them to agda2-mode-hook. For instance, if you do not want to use the Agda input method (for writing various symbols like ∀≥ℕ→π⟦⟧) you can add the following to your .emacs:

(add-hook 'agda2-mode-hook
          '(lambda ()
            ; If you do not want to use any input method:
            (deactivate-input-method)
            ; (In some versions of Emacs you should use
            ; inactivate-input-method instead of
            ; deactivate-input-method.)

Note that, on some systems, the Emacs mode changes the default font of the current frame in order to enable many Unicode symbols to be displayed. This only works if the right fonts are available, though. If you want to turn off this feature, then you should customise the agda2-fontset-name variable.

The colors that are used to highlight Agda syntax and errors can be adjusted by typing M-x customize-group RET agda2-highlight RET in Emacs and following the instructions.

Keybindings

Notation for key combinations

The following notation is used when describing key combinations:

C-c

means hitting the c key while pressing the Ctrl key.

M-x

means hitting the x key while pressing the Meta key, which is called Alt on many systems. Alternatively one can type Escape followed by x (in separate key strokes).

RET

is the Enter, Return or ⏎ key.

SPC

is the space bar.

By default, terms and types printed by interactive commands will be simplified by evaluating certain functions. Specifically, only those functions that match on a constructor pattern or a projection copattern will be reduced, as well as primitive functions of Agda. For example, (suc x) + y will be simplified to suc (x + y) but id 42 will be printed as is. The level of normalisation of commands that print a term or type can be modified by prefixing the command by one or more repetitions of C-u:

  • C-u to print the term without any simplification.

  • C-u C-u to print the full normal form.

  • C-u C-u C-u to print the weak-head normal form.

Global commands

These commands can be invoked both from within or outside of a hole. When invoked from within a hole and whenever it makes sense, they limit their action to the hole and take context and content of the hole into account.

C-c C-l

Load file. This type-checks the contents of the file, and replaces each occurrence of a question mark ? or a hole marker {! !} by a freshly created hole.

C-c C-x C-c

Compile file. This will compile an Agda program with a main function using a given backend (the GHC backend is used by default).

C-c C-i

Call a given backend’s top-level (or hole) interaction command (if any).

C-c C-x C-q

Quit, kill the Agda process.

C-c C-x C-r

Kill and restart the Agda process.

C-c C-x C-s

Switch to a different Agda version.

C-c C-x C-a

Abort a command.

C-c C-x C-d

Remove goals and highlighting (deactivate).

C-c C-x C-h

Toggle display of hidden arguments.

C-c C-x C-i

Toggle display of irrelevant arguments.

C-c C-f

Move to next goal (forward).

C-c C-b

Move to previous goal (backwards).

C-c C-?

Show all goals.

C-c C-=

Show constraints.

C-c C-s

Solve constraints. Tries to fill holes with existing meta variable solutions (as displayed by C-c C-=).

C-c C-a

Automatic Proof Search (Auto) Tries to fill holes by automatic type-directed term synthesis.

C-c C-d

Infer (deduce) type. The system asks for a term and infers its type. When executed inside a hole, it will instead take the contents of the hole as input (if any).

C-c C-n

Compute normal form. The system asks for a term which is then evaluated. When executed inside a hole, it will instead take the contents of the hole as input (if any).

C-u C-c C-n

Compute normal form, ignoring abstract and NON_TERMINATING.

C-u C-u C-c C-n

Compute and print normal form of show <expression>.

C-u C-u C-u C-c C-n

Compute weak head normal form.

C-c C-o

Display contents of the given module.

C-c C-w

Why in scope, given a defined name returns how it was brought into scope and its definition.

C-c C-z

Search Definitions in Scope

C-c C-x M-;

Comment/uncomment rest of buffer.

Commands in context of a goal

The following commands only work (and make sense) inside of a hole.

Commands expecting input (for example which variable to case split) will either use the text inside the goal or ask the user for input.

C-c C-SPC

Give (fill goal)

C-c C-r

Refine. Checks whether the return type of the expression e in the hole matches the expected type. If so, the hole is replaced by e { }1 ... { }n, where a sufficient number of new holes have been inserted. If the hole is empty, then the refine command instead inserts a lambda or constructor (if there is a unique type-correct choice).

C-c C-m

Elaborate and Give (fill goal with normalized expression). Takes the same C-u prefixes as C-c C-n.

C-c C-c

Case split. If the cursor is positioned in a hole which denotes the right hand side of a definition, then this command automatically performs pattern matching on variables of your choice. When given several variables (separated by spaces) it will case split on the first and then continue by case splitting on the remaining variables in each newly created clause. When given no variables, it will introduce a new variable if the target type is a function type, or introduce a new copattern match if the target type is a record type (see Copatterns). When given the special symbol ., it will expand the ellipsis ... in the clause (see With-Abstraction).

C-c C-h

Compute type of helper function and add type signature to kill ring (clipboard).

C-c C-t

Goal type.

C-c C-e

Context (environment).

C-c C-,

Goal type and context. Shows the goal type, i.e. the type expected in the current hole, along with the types of locally defined identifiers.

C-c C-.

Goal type, context and inferred type.

C-c C-;

Goal type, context and checked term.

Other commands

TAB

Indent current line, cycles between points.

S-TAB

Indent current line, cycles in opposite direction.

M-.

Go to definition of identifier under point.

Middle mouse button

Go to definition of identifier clicked on.

M-*

Go back (Emacs < 25.1).

M-,

Go back (Emacs ≥ 25.1).

Unicode input

How can I write Unicode characters using Emacs?

The Agda Emacs mode comes with an input method for easily writing Unicode characters. Most Unicode character can be input by typing their corresponding TeX/LaTeX commands, eg. typing \lambda will input λ. Some characters have key bindings which have not been taken from TeX/LaTeX (typing \bN results in ℕ being inserted, for instance), but all bindings start with \.

To see all characters you can input using the Agda input method type M-x describe-input-method RET Agda or type M-x agda-input-show-translations RET RET (with some exceptions in certain versions of Emacs).

If you know the Unicode name of a character you can input it using M-x ucs-insert RET (which supports tab-completion) or C-x 8 RET. Example: Type C-x 8 RET not SPACE a SPACE sub TAB RET to insert the character “NOT A SUBSET OF” (⊄).

(The Agda input method has one drawback: if you make a mistake while typing the name of a character, then you need to start all over again. If you find this terribly annoying, then you can use Abbrev mode instead. However, note that Abbrev mode cannot be used in the minibuffer, which is used to give input to many Agda and Emacs commands.)

The Agda input method can be customised via M-x customize-group RET agda-input.

OK, but how can I find out what to type to get the … character?

To find out how to input a specific character, eg from the standard library, position the cursor over the character and type M-x describe-char or C-u C-x =.

For instance, for ∷ I get the following:

            character: ∷ (displayed as ∷) (codepoint 8759, #o21067, #x2237)
    preferred charset: unicode (Unicode (ISO10646))
code point in charset: 0x2237
               script: symbol
               syntax: w      which means: word
             category: .:Base, c:Chinese
             to input: type "\::" with Agda input method
          buffer code: #xE2 #x88 #xB7
            file code: #xE2 #x88 #xB7 (encoded by coding system utf-8-unix)
              display: by this font (glyph code)
    x:-misc-fixed-medium-r-normal--20-200-75-75-c-100-iso10646-1 (#x2237)

Character code properties: customize what to show
  name: PROPORTION
  general-category: Sm (Symbol, Math)
  decomposition: (8759) ('∷')

There are text properties here:
  fontified            t

Here it says that I can type \:: to get a ∷. If there is no “to input” line, then you can add a key binding to the Agda input method by using M-x customize-variable RET agda-input-user-translations.

Show me some commonly used characters

Many common characters have a shorter input sequence than the corresponding TeX command:

  • Arrows: \r- for →. You can replace r with another direction: u, d, l. Eg. \d- for ↓. Replace - with = or == to get a double and triple arrows.

  • Greek letters can be input by \G followed by the first character of the letters Latin name. Eg. \Gl will input λ while \GL will input Λ.

  • Negation: you can get the negated form of many characters by appending n to the name. Eg. while \ni inputs ∋, \nin will input ∌.

  • Subscript and superscript: you can input subscript or superscript forms by prepending the character with \_ (subscript) or \^ (superscript). Eg. g\_1 will input g₁. Note that not all characters have a subscript or superscript counterpart in Unicode.

Note: to introduce multiple characters involving greek letters, subscripts or superscripts, you need to prepend \G, \_ or \^ respectively before each character.

Some characters which were used in this documentation or which are commonly used in the standard library (sorted by hexadecimal code):

Hex code

Character

Short key-binding

TeX command

00AC

¬

\neg

00D7

×

\x

\times

02E2

ˢ

\^s

03BB

λ

\Gl

\lambda

041F

П

0432

в

0435

е

0438

и

043C

м

0440

р

0442

т

1D62

ᵢ

\_i

2032

′

\'1

\prime

207F

ⁿ

\^n

2081

₁

\_1

2082

₂

\_2

2083

₃

\_3

2084

₄

\_4

2096

ₖ

\_k

2098

ₘ

\_m

2099

ₙ

\_n

Hex code

Character

Short key-binding

TeX command

2113

ℓ

\ell

Hex code

Character

Short key-binding

TeX command

2115

ℕ

\bN

\Bbb{N}

2191

↑

\u

\uparrow

2192

→

\r-

\to

21A6

↦

\r-|

\mapsto

2200

∀

\all

\forall

2208

∈

\in

220B

∋

\ni

220C

∌

\nin

2218

∘

\o

\circ

2237

∷

\::

223C

∼

\~

\sim

2248

≈

\~~

\approx

2261

≡

\==

\equiv

2264

≤

\<=

\le

2284

⊄

\subn

228E

⊎

\u+

\uplus

2294

⊔

\lub

22A2

⊢

\|-

\vdash

22A4

⊤

\top

22A5

⊥

\bot

266D

♭

\b

266F

♯

\#

27E8

⟨

\<

27E9

⟩

\>

Hex code

Character

Short key-binding

TeX command

2983

⦃

\{{

2984

⦄

\}}

2985

⦅

\((

2986

⦆

\))

Hex code

Character

Short key-binding

TeX command

2C7C

ⱼ

\_j

Background highlighting

Agda uses various background colors to indicate specific errors or warnings in your code. Specifically, the following colors are used:

  • A yellow background indicates unsolved metavariables (see Metavariables) or unsolved constraints.

  • A light salmon (pink-orange) background indicates an issue with termination or productivity checking (see Termination Checking).

  • A wheat (light yellow) background indicates an issue with coverage checking (see Coverage Checking).

  • A peru (brown) background indicates an issue with positivity checking (see Positivity Checking).

  • An orange background indicates a type signature with a missing definition.

  • A light coral (darker pink) background indicates a fatal warning

  • A grey background indicates unreachable or dead code, and for shadowed variable names in telescopes.

  • A white smoke (light grey) background indicates a clauses that does not hold definitionally (see Case trees).

  • A pink background indicates an issue with confluence checking of rewrite rules (see Confluence checking).