<div dir="ltr">Thanks Mateusz,<div>That helped a lot and I made some progress towards my modest</div><div>goal of putting some Agda code in a beamer presentation.</div><div><br></div><div>I used <span style="font-family:arial,sans-serif;font-size:16px">agda --latex and it made a directory latex/ containing the .tex file.</span></div>
<div><span style="font-family:arial,sans-serif;font-size:16px"><br></span></div><div><span style="font-family:arial,sans-serif;font-size:16px">(I spend a lot of time trying to look for the .tex output in current directory. Before that, I spent</span></div>
<div><span style="font-family:arial,sans-serif;font-size:16px">some time trying to figure out why agda --latex was saying that the flag --latex</span></div><div><span style="font-family:arial,sans-serif;font-size:16px">is unrecognized. It turned out that --latex is not available in my older version (2.3.0)</span><span style="font-family:arial,sans-serif;font-size:16px">)</span></div>
<div><span style="font-family:arial,sans-serif;font-size:16px"><br></span></div><div><span style="font-family:arial,sans-serif;font-size:16px">The .tex file compiles correctly and produces beautiful output.</span></div><div>
<span style="font-family:arial,sans-serif;font-size:16px">Then, I copied relevant code to my beamer slide and got the following error:</span></div><div><span style="font-family:arial,sans-serif;font-size:16px">--------------</span><br>
</div><div><font face="arial, sans-serif"><span style="font-size:16px">! Package biblatex Error: Incompatible package 'ucs'.See the biblatex package documentation for explanation.Type H <return> for immediate help.... \begin{document}</span></font><br>
</div><div>-----------</div><div>It appears that agda.sty needs the ucs package.</div><div>I need biblatex to show citations as footnotes. I could't find any alternative to biblatex.</div><div>I am not sure how to fix this issue.</div>
<div>It would be great if emacs could export to latex whatever it is rendering. I couldn't find any way to do that. I tried using htmlfontify-buffer, but it replaced all special characters with "?".</div><div>
<br></div><div>Any ideas about fixing this problem would be greatly appreciated.<br></div><div><br></div><div>Thanks,</div><div><br></div></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 8:37 PM, Mateusz Kowalczyk <span dir="ltr"><<a href="mailto:fuuzetsu@fuuzetsu.co.uk" target="_blank">fuuzetsu@fuuzetsu.co.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">On 29/11/13 00:19, Abhishek Anand wrote:<br>
> Sorry for asking a beginner question.(Can't seem to find it on google).<br>
><br>
> How does one generate a .lagda file from a .agda file<br>
> When I compile in windows, I get a .exe file<br>
> I also see some .agdai files<br>
><br>
<br>
</div>You don't generate .lagda files, you write your code in them. So for<br>
example, instead of writing in MyModule.agda, you would write in<br>
MyModule.lagda and then compile that. The difference is that you can use<br>
the literate syntax when using the .lagda file extension and the<br>
compiler should know what to do when it sees .lagda.<br>
<span class="HOEnZb"><font color="#888888"><br>
<br>
--<br>
Mateusz K.<br>
</font></span><div class="HOEnZb"><div class="h5">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>