[Agda] Writing a paper in Literate Agda

[Tillmann Rendel]

Hi,

Alan Jeffrey wrote:
> I decided to try an
> experiment of actually writing the paper in Literate Agda, so the
> mathematics in the paper is actually what has been validated.

Did you consider using

   agda --latex

or

   lhs2tex --agda

to generate a *.tex file from a *.lagda file?

   Tillmann