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$
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$– TyberiusFeb 8, 2022 at 21:04
-
$\begingroup$ @Tyberius clarified undo the close vote $\endgroup$– FmbalbuenaFeb 8, 2022 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$– TyberiusFeb 8, 2022 at 21:07
-
$\begingroup$ @Tyberius Please answer instead $\endgroup$– FmbalbuenaFeb 8, 2022 at 21:08
-
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 ♦Feb 9, 2022 at 9:01
|
Show 1 more comment
2 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$ 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$ 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.
