Introduction

Getting Started

Requirements

• Haskell programming language

• Haskell Cabal

• Agda programming language

  • version >= 2.6.4 && < 2.6.5

• Agda standard library

• Agda library agda2hs

  • this Agda library is included in the agda2hs repository; see agda2hs.agda-lib

  • you can navigate the library in HTML format, along with a comprehensive test suite

Installation

Let DIR be the directory in which you start running these shell commands.

# clone the repository locally
git clone git@github.com:agda/agda2hs.git

# build agda2hs with cabal
cd agda2hs
cabal install

# register the agda2hs Agda library
echo $(pwd)/agda2hs.agda-lib >> ~/.agda/libraries
# register the agda2hs Agda library as a default
echo agda2hs >> ~/.agda/defaults

Running agda2hs

To run agda2hs, run

agda2hs <path>/<name>.agda [-o <outputDir>]

which, for all dependencies of that Agda file, compiles and writes

[<outputDir>/]<modulePath>.hs

Using agda2hs with Stack

You can use agda2hs with the Haskell Stack tool.

TODO: integrate agda2hs as a preprocessor for stack