[Agda] Writing a paper in Literate Agda
ajeffrey at bell-labs.com
Thu Nov 28 16:51:27 CET 2013
Yes I did, but I'd like to control the TeX setting myself.
In terms of tool support, the one thing I did sorely miss is the ability
to run LaTeX from emacs's Agda mode. Does anyone know of an easy way to
On 11/28/2013 04:29 AM, Tillmann Rendel wrote:
> 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
> lhs2tex --agda
> to generate a *.tex file from a *.lagda file?
> Agda mailing list
> Agda at lists.chalmers.se
More information about the Agda