[Agda] Writing a paper in Literate Agda

[Ulf Norell]

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