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$
$\endgroup$
5
-
$\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$– TyberiusCommented 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$– TyberiusCommented Feb 8, 2022 at 21:07
-
$\begingroup$ @Tyberius Please answer instead $\endgroup$– FmbalbuenaCommented 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$– TyberiusCommented 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 ♦Commented Feb 9, 2022 at 9:01
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
2
Given that you arrived here "having no idea" how to run it, the easiest might be:
- Install Visual Studio Code
- Install
banacorn.agda-modepackage in Visual Studio Code. - Enable
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
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$ Commented 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$ Commented Feb 9, 2022 at 16:17
$\begingroup$
$\endgroup$
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.
$\begingroup$
$\endgroup$
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/
