6
$\begingroup$

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?

$\endgroup$
6
  • $\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 at 21:04
  • $\begingroup$ @Tyberius clarified undo the close vote $\endgroup$
    – Fmbalbuena
    Feb 8 at 21:05
  • $\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 at 21:07
  • $\begingroup$ @Tyberius Please answer instead $\endgroup$
    – Fmbalbuena
    Feb 8 at 21:08
  • 2
    $\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 at 9:01

2 Answers 2

16
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ How does one "Enable agdaMode.connection.agdaLanguageServer in the package"? $\endgroup$ Feb 8 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 at 16:17
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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