# How to run Agda?

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?

• 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? Feb 8 at 21:04
• @Tyberius clarified undo the close vote Feb 8 at 21:05
• 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. Feb 8 at 21:07
• @Tyberius Please answer instead Feb 8 at 21:08
• 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.
– Trebor
Feb 9 at 9:01

## 2 Answers

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

1. Install Visual Studio Code
2. Install banacord.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-l and then Ctrl-c.

• How does one "Enable agdaMode.connection.agdaLanguageServer in the package"? Feb 8 at 23:52
• 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. Feb 9 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.