[Agda] c-c c-l + import
Serge D. Mechveliani
mechvel at botik.ru
Tue Apr 23 20:24:26 CEST 2013
People,
I am trying to use the Agda interactive environvent under Emacs,
by following the instructions on Quick Editing Guide on the Web.
I edit T.agda in emacs, with using the Agda mode.
If T.agda does not import the Library, then c-c c-l seems to
type-check.
But if T.agda uses something from Standard Library, then it reports
something about the library module.
On the other hand, agda -c $agdaLibOpt T.agda
does work in the command line.
How to bring the library modules to the emacs interactive shell?
Thanks,
------
Sergei
More information about the Agda
mailing list