[Agda] Writing a paper in Literate Agda

Abhishek Anand abhishek.anand.iitg at gmail.com
Wed Dec 18 17:13:50 CET 2013


Is there was way to get agda --latex or agda --html to produce output even
when there are holes in the source file?

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


On Mon, Dec 2, 2013 at 5:52 AM, Nils Anders Danielsson <nad at cse.gu.se>wrote:

> On 2013-12-01 22:33, Abhishek Anand wrote:
>
>> It appears that agda.sty needs the ucs package.
>> I need biblatex to show citations as footnotes. I could't find any
>> alternative to biblatex.
>> I am not sure how to fix this issue.
>> 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 "?".
>>
>> Any ideas about fixing this problem would be greatly appreciated.
>>
>
> I haven't used agda --latex in anger, but I can see that agda.sty
> doesn't use ucs if you use XeLaTeX (which supports UTF-8 out of the
> box).
>
> --
> /NAD
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131218/3d397521/attachment.html


More information about the Agda mailing list