[Agda] Writing a paper in Literate Agda

[Andreas Abel]

This seems to be related to issue 964

   http://code.google.com/p/agda/issues/detail?id=964

Agda refuses to write an interface file when there are metas left.

On 18.12.2013 17:13, Abhishek Anand wrote:
> 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
> <mailto: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
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/