Alonzo

To invoke Alonzo call the batch tool with the flag -c. For instance,

  agda -c Thing.agda

This will generate a Haskell file Thing.hs which can then be compiled by ghc. If Thing depends on other Agda modules they will have to be compiled as well. The prerequisites are:

• The batch tool (src/main).
• The runtime system for the compiler (src/rts).

Both are built using the standard cabal incantations:

  runhaskell Setup.hs configure
  runhaskell Setup.hs build
  sudo runhaskell Setup.hs install

If the Agda module contains a function main, Alonzo assumes that this is the Main module and that the type (after compilation) of main is IO ().