[Agda] Writing a paper in Literate Agda

[Alan Jeffrey]

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 
do this?

A.

On 11/28/2013 04:29 AM, Tillmann Rendel wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda