[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