‘Hello world’ in Agda

This section contains two minimal Agda programs that can be used to test if you have installed Agda correctly: one for using Agda interactively as a proof assistant, and one for compiling Agda programs to an executable binary. For a more in-depth introduction to using Agda, see A taste of Agda or the list of tutorials.

Hello, Agda!

Below is is a small ‘hello world’ program in Agda (defined in a file hello.agda).

data Greeting : Type where
  hello : Greeting

greet : Greeting
greet = hello

This program defines a data type called Greeting with one constructor hello, and a function definition greet of type Greeting that returns hello.

To load the Agda file, open it in Emacs and load it by pressing C-c C-l (Ctrl+c followed by Ctrl+l). You should now see that the code is highlighted and there should be a message *All done*. If this is the case, congratulations! You have correctly installed Agda and the Agda mode for Emacs. If you also want to compile your Agda programs, continue with the next section.