[Agda] agda options under emacs

[Nils Anders Danielsson]

On 2009-12-13 13:28, Florent Balestrieri wrote:
> I wish to use the command line option --allow-unsolved-meta
> when running agda interactively within emacs (and didn't find
> out how).

You can use an OPTIONS pragma, but this is not very useful, because the
--allow-unsolved-metas flag only applies to the top-level module and the
Emacs mode allows unsolved metas in the top-level module anyway.

> Now agda 2.2.4 won't typecheck a module which imports another
> uncompleted module, complaining about those unsolved meta
> variables. Is there a way to make agda more flexible about
> those things?

No. (Unless you modify the implementation.) You can use postulates
instead.

-- 
/NAD