Developed for my thesis "Programs for Free: Towards a formalization of Implicit Resolution in Scala". Building on top of earlier work by (Oliveira, Bruno CdS, et al.).
The code has been compiled against agda 2.4.2.3 and beyond and should be compatible with the latest version of the agda stdlib.
Install the standard library somewhere by cloning it and add the following snippet to your agda libraries file
~/.agda/libraries:
<AGDA_STDLIB_PATH>/standard-library.agda-lib
Typechecking the proofs is as simple as:
make
This generates the browsable, syntax highlighted source in doc/html/:
make doc