banacorn/agda-mode-vscode

agda-mode on VS Code

187

stars

2,367

commits

ReScript

primary language

Sep 10, 2026

updated

marketplace.visualstudio.com/items?itemName=banacorn.agda-mode

agda

agda-mode

reasonml

vscode

vscode-extension

Browse cluster: VS Code Language Extensions →

README

agda-mode on VS Code

Installation

If you have Agda properly installed (to check this in your terminal, type agda and see if it's on your machine). Open an Agda file and you should be able to load it by typing C-c C-l.

It's okay if you don't have Agda installed, we can also download and install Agda Language Server for you on Windows, macOS, or Ubuntu.

You can install multiple versions of Agda or ALS by adding more paths to agdaMode.connection.paths in the settings, and switch between them with C-c C-r.

Extension Activation

To activate the extension, open an Agda file, and trigger either of these 2 commands:

Command	Keymap
load	`C-c` `C-l`
activate unicode input method	`\`

See the next section for the exhaustive list of other commands. You will get command ... not found if you try to trigger other commands without activating the extension first.

Commands

C-c stands for "press Ctrl and c at the same time"
When it comes to combos like C-c C-l, you can often slur them into "hold Ctrl while pressing c and then l"

Commands working with terms or types (marked with the 🎚 emoji below) can be prefixed with C-u to compute without further normalisation, with C-u C-u to compute normal forms, and C-u C-u C-u to compute weak-head normal forms like in Emacs.

Global commands

Command	Keymap
load	`C-c` `C-l`
compile	`C-c` `C-x` `C-c`
quit	`C-c` `C-x` `C-q`
quit and restart	`C-c` `C-x` `C-r`
toggle display of hidden arguments	`C-c` `C-x` `C-h`
toggle display of irrelevant arguments	`C-c` `C-x` `C-i`
show constraints 🎚¹	`C-c` `C-=`
solve constraints 🎚	`C-c` `C-s`
show all goals 🎚	`C-c` `C-?`
move to next goal (forward)	`C-c` `C-f`
move to previous goal (backwards)	`C-c` `C-b`
infer type 🎚	`C-c` `C-d`
module contents 🎚	`C-c` `C-o`
search definitions in scope 🎚	`C-c` `C-z`
compute normal form 🎚	`C-c` `C-n`
switch to a different installation of Agda or ALS	`C-x` `C-s`
Unicode symbol input sequences lookup	`C-x` `C-=`

Commands in context of a goal

Command	Keymap
give (fill goal)	`C-c` `C-SPC`
refine	`C-c` `C-r`
elaborate and give 🎚	`C-c` `C-m`
auto 🎚	`C-c` `C-a`
case split	`C-c` `C-c`
compute helper function type and copy 🎚	`C-y` `C-h`
goal type 🎚	`C-c` `C-t`
context (environment) 🎚	`C-c` `C-e`
infer type 🎚	`C-c` `C-d`
goal type and context 🎚	`C-c` `C-,`
goal type, context and inferred term 🎚	`C-c` `C-.`
goal type, context and checked term 🎚	`C-c` `C-;`
module contents 🎚	`C-c` `C-o`
compute normal form 🎚	`C-c` `C-n`
why in scope	`C-c` `C-w`

Commands yet to be implemented

Command	Keymap
abort a command	`C-x` `C-a`
remove goals and highlighting	`C-x` `C-d`
comment/uncomment rest of buffer

Unicode Input

Pretty much the same like on Emacs. Press backslash "\" and you should see a keyboard popping up in the panel, with key suggestions and symbol candidates. Use arrow keys to explore and navigate between the candidates (if there's any).

Unicode input also works in the input prompt, though it's a bit less powerful.

If you are having trouble typing the backslash "\", go to "Preferences: Open Keyboard Shortcuts" and configure the keybinding of "Agda: Activate input method" (agda-mode.input-symbol[Activate]). By default, this command is bound to VS Code's layout-independent [Backslash] scan code.

Cancel agdaMode.inputMethod.enable in the settings to disable the input method.

Debug Buffer

Execute Agda: Open Debug Buffer in the Command Palette to open it. The number at the end of each message indicates its verbosity.

Troubleshooting

Agda files won't load, commands don't work

Please go to "Preferences: Open Keyboard Shortcuts" and see if any extension is fighting for the same key combo. You're probably a victim of the Vim extension.