[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