[Agda] Typechecking a module using Haskell

[Lyndon Maydwell]

Are you asking how you would normally type-check an Agda module?


If so, there are a few steps that are outlined on the Agda wiki:
http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Download

This requires installing some variant of Haskell (usually the Haskell
platform: http://hackage.haskell.org/platform/), then installing Agda
with cabal.

Usually you set up Emacs to use Haskell and Agda, then check files by
loading them using C-c C-l (see the wiki).

However there is an Agda-Executable that you can use to check programs
in a stand-alone fashion that can be installed with "cabal install
Agda-executable".

You will probably also want to install the standard library:
http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.StandardLibrary.


Once this is all set up, if you want to take the Emacs path, follow
the wiki instructions for setting Emacs up to work with Agda, then
just edit the file "emacs my_module.agda", and once it is open without
any errors popping up, hit <Ctrl>-c <Ctrl>-l.

That should highlight the file and indicate that the module has been
checked successfully.

I went through the process of installing Agda on a new machine again
literally half an hour ago and it was the smoothest time yet. Good
luck!


On Sat, Jun 16, 2012 at 10:44 PM, TOmmo Ceee <tm1rbrt at gmail.com> wrote:
> Could someone please talk me through how to load and typecheck a module
> using the agda package from hackage please.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>