[Agda] Writing a paper in Literate Agda

Ulf Norell ulf.norell at gmail.com
Wed Dec 18 22:39:38 CET 2013

On Wed, Dec 18, 2013 at 5:13 PM, Abhishek Anand <
abhishek.anand.iitg at gmail.com> wrote:

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

Just pass the option --allow-unsolved-metas and Agda will happily generate
html or latex from a file with holes.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131218/51920c44/attachment.html

More information about the Agda mailing list