<div dir="ltr">Sorry for asking a beginner question.(Can't seem to find it on google).<div><br></div><div>How does one generate a .lagda file from a .agda file</div><div>When I compile in windows, I get a .exe file</div>
<div>I also see some .agdai files</div><div><br></div><div class="gmail_extra"><br clear="all"><div><div>-- Abhishek</div><a href="http://www.cs.cornell.edu/~aa755/" target="_blank">http://www.cs.cornell.edu/~aa755/</a></div>
<br><br><div class="gmail_quote">On Thu, Nov 28, 2013 at 5:29 AM, Tillmann Rendel <span dir="ltr"><<a href="mailto:rendel@informatik.uni-marburg.de" target="_blank">rendel@informatik.uni-marburg.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<div class="im"><br>
<br>
Alan Jeffrey wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I decided to try an<br>
experiment of actually writing the paper in Literate Agda, so the<br>
mathematics in the paper is actually what has been validated.<br>
</blockquote>
<br></div>
Did you consider using<br>
<br>
agda --latex<br>
<br>
or<br>
<br>
lhs2tex --agda<br>
<br>
to generate a *.tex file from a *.lagda file?<span class="HOEnZb"><font color="#888888"><br>
<br>
Tillmann</font></span><div class="HOEnZb"><div class="h5"><br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div></div>