I want to run Agda, but I do not know how to run functions. I need to run "Hello, World!"; how can I do this?

  • $\begingroup$ You may have to clarify what you mean. Do you just mean run some simple example (e.g. hello world agda) or are you trying to do something specific? $\endgroup$
    – Tyberius
    Feb 8, 2022 at 21:04
  • $\begingroup$ Did you check the link from my comment? If you followed the install instructions from their documentation, following the tutorial there would be the logical next step. $\endgroup$
    – Tyberius
    Feb 8, 2022 at 21:07
  • $\begingroup$ @Tyberius Please answer instead $\endgroup$
    – Fmbalbuena
    Feb 8, 2022 at 21:08
  • $\begingroup$ I'm a complete beginner with Proof Assistants, so the best I can offer you is the very short tutorial in that link. $\endgroup$
    – Tyberius
    Feb 8, 2022 at 21:14
  • 3
    $\begingroup$ I think if such questions can be answered with a direct link it should be treated in the way of StackOverflow. Otherwise there should be descriptions of the resources you already read about (and failed to follow), because you don't want answerers to give you something you tried. $\endgroup$
    – Trebor
    Feb 9, 2022 at 9:01

3 Answers 3


Given that you arrived here "having no idea" how to run it, the easiest might be:

  1. Install Visual Studio Code
  2. Install banacorn.agda-mode package in Visual Studio Code.
  3. Enable agdaMode.connection.agdaLanguageServer in the package and it will install Agda for you.

With some luck, you're all set to go. Open a file Cow.agda, copy this into it:

module Cow where

  data Bull : Set where
    horn : Bull
    tail : Bull

Press Ctrl-c and then Ctrl-l, which will invoke type-checking in agda-mode.

  • $\begingroup$ How does one "Enable agdaMode.connection.agdaLanguageServer in the package"? $\endgroup$ Feb 8, 2022 at 23:52
  • $\begingroup$ You go to preferences/settings and search for agdaLanguageServer, then enable it. But I think the Agda package asks you at some point if you'd like to enable the language server. $\endgroup$ Feb 9, 2022 at 16:17

One possibility is to use Emacs. Quoting the book Programming Language Foundations in Agda:

Agda ships with the editor support for Emacs built-in, so if you’ve installed Agda, all you have to do to configure Emacs is run:

agda-mode setup
agda-mode compile

Open a .agda file, and load and type-check the code in the file using the key combination: C-c C-l (which stands for Ctrl-c Ctrl-l). Other useful key combinations are described in the documentation here.


It's true that a full deployment of Agda on a computer is more inconvenient compared to other proof assistants, but if you just want to try it out, you can try the browser version of Agda: https://agdapad.quasicoherent.io/


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.