Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time


To compile and run the main program, do the following in the agda directory. Note that you will need to modify Main.agda as it hardcodes some local information. Also you will need to cabal install --lib the following libraries:

  • HCodecs
  • sbv

To use synthesis features, Z3 must also be installed and in the path.

I am using the latest development versions of Agda/Agda-Stdlib/Cubical and GHC 9.2.2 but it may work with other versions as well. No support is provided if it doesn't work.

  • agda -c Main.agda
  • ./Main

To make slides from source, Agda, XeLaTeX and the XITS font must be installed.

  • In the agda directory, run agda --latex Pnwplse.lagda.
  • Then in the slides directory, run xelatex pnwplse.tex. This may need to be run more than once, for example if the number of pages changes.

Note that \setsansfont must be added to the default agda.sty file if the file is updated from the latest Agda distribution.