[Agda] Writing a paper in Literate Agda

[Abhishek Anand]

Sorry for asking a beginner question.(Can't seem to find it on google).

How does one generate a .lagda file from a .agda file
When I compile in windows, I get a .exe file
I also see some .agdai files


-- Abhishek
http://www.cs.cornell.edu/~aa755/


On Thu, Nov 28, 2013 at 5:29 AM, Tillmann Rendel <
rendel at informatik.uni-marburg.de> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131128/c8760e78/attachment.html