[Agda] agda options under emacs

Florent Balestrieri fyb at cs.nott.ac.uk
Sun Dec 13 14:28:52 CET 2009


Hello,

I wish to use the command line option --allow-unsolved-meta
when running agda interactively within emacs (and didn't find
out how).

I'm writing several interdependent modules at once and
because I have priorities, I don't fill every definition :
some are just question marks with which I would deal later.

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?

Cheers
-- FB



More information about the Agda mailing list