See report.pdf for documentation.
The code was ran and tested against Idris2, version 0.5.1
Idris might not recognize literate Idris files with .tex extension when resolving import,
but it will happily compile them when called directly.
So, if you encounter errors, please run the build.sh script.
If you don't have bash on your system, you can still consult the aforementioned build script
for the order in which to manually compile the modules.