Getting Agda up and running

TLDR : Agda + VSCode for HoTT summer school.

Note: This is for the HoTT summer school. You can also use this for agda too, but its main purpose is different. Skip to step 5 to just run it.

My system is running Pop-Os 22.04, so I used the Ubuntu installation for everything. I cannot tell what errors might pop up in other OSes. Do take care.

For the two people in the universe who actually use Agda, here is a tutorial on how to get it up and running on VSCode. I know you can use emacs, but for now let’s not use it. (Could add later, leave me alone).

Step 1

Install Agda + agda-mode.

This link should get you started, but if you’d rather not wade through said installation……yeah you have to. Install it. It’s a few lines.

Step 2

Install VSCode. Since that’s what we’re using (presumably).

Step 3

Since this is specifically for the HoTT summer school, go clone the repo given below.

git clone

If you dont have git, download the file instead from here.

Note: This file is important to have for one reason. It contains certain libraries. You cannot run the exercises without these.

Step 4

Install the following 2 extensions on VSCode

Extension 1
Name: agda-mode
Id: banacorn.agda-mode
Description: agda-mode on vscode
Version: 0.3.9
Publisher: Ting-Gian LUA
VS Marketplace Link:
Extension 2
Name: language-agda
Id: j-mueller.agda
Description: Syntax highlighting and snippets for agda
Version: 0.1.7
Publisher: j-mueller
VS Marketplace Link:

Note: Searching the term ‘agda’ in the extensions tab of VSCode should give you these both. Installing is a single button click.

Step 5

You can now use VSCode as you wish. However, here are a few points to keep in mind to actually run the programs. I will give an example below.

  1. (Ctrl-C + Ctrl-L) is your best friend (capital for emphasis. small c and small l will suffice). This actually runs through the file and executes it. It also restarts the agda process (apparently).
  2. {!!} are goals. (Ctrl-C + Ctrl-space) will fill these holes with your variables/outputs/whatever. You will have to type in them and then execute the shortcut. Empty holes become goals.
  3. (Ctrl-Shift-P + Agda:Case) :: This is not a shortcut, but will case split for you based on the variables in the holes (do not C-c C-space them if you wish to case split).

Note: VSCode does not operate like a normal text editor when editing the agda files. (I’ll assume that you’re editing There are special commands to use. Hence, it could be easy to screw up said file. Dont worry too much, let it be. (Redownload file if required).


For, open the file (within the previously downloaded folder) in VSCode. Run the first command (for testing).

All goals
C-c + C-l will give you either this or “All Done” (or something similar)

Case Splitting

To split case, look at the first problem.

_&&'_ : Bool → Bool → Bool
a &&' b = {!0!}

Change it to the below

_&&'_ : Bool → Bool → Bool
a &&' b = {!a b0!}

Now, put your cursor inside the brackets (between the exclamation points).

When you press Ctrl-Shift-P, that’ll open a text field at the top. Search Agda:case within said text field. You’ll find the option to split case.

It’ll come on top.

It will now change into the below.

Screenshot of my code

Note: You don't have to use this. A convenience rather than a necessity.

Solving goals

To solve goals, enter the values within the brackets.

Screenshot of my code

C-c + C-space will finish the goal (as seen below).

Screenshot of my code

Rerun C-c C-l to see results.

Happy solving (and not trying to fling your laptop) !

Note: VSCode can be really really picky about what commands it chooses to recognise. C-c C-space doesn't work for me sometimes and it only works again when I close VSCode and the terminal I launched it from.

As I mentioned before, take care. Worst case, restart system (Not ideal, but I have no solution for now).



Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Aditya Sujith Gudimetla

I do stuff. Like stuff about policy. And book stuff. And gaming stuff. And stuff about life. And stuff about stuff.