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?
Given that you arrived here "having no idea" how to run it, the easiest might be:
- Install Visual Studio Code
banacorn.agda-modepackage in Visual Studio Code.
agdaMode.connection.agdaLanguageServerin 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
Ctrl-c and then
Ctrl-l, which will invoke type-checking in agda-mode.
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
.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.