LaTeX macros for Literate Agda
This repository contains the macros that I use for writing papers in Literate Agda.
These macros have a different aim than agda.sty, which is to allow a .lagda
file to be used as part of a mathematical paper, typeset in LaTeX, but with the
mathematics typechecked by Agda. Even if all this is doing is helping reduce
typos, this is better than nothing!