agda/examples/outdated-and-incorrect/Alonzo

== Using Alonzo ==

agda --alonzo File.agda

or

agda -c File.agda

produces File.hs

compile it with
ghc -c File.hs

The main module should contain the function mainS : String, compile it with

ghc --make -main-is File.main File.hs

There is a shell script "almake" that will do both, provided you have
compiled all dependencies beforehand.

Prerequisites

You need the following runtime files:

RTS.hs RTN.hs RTP.hs
RTN.agda RTP.agda

NEVER run agda -c on RT* files as it will destroy the corresponding .hs files

There is a "runtime" target in the Makefile, so running

make runtime

will compile the runtime files for you.

There is a small prelude included, you can compile it with

make prelude