[Agda] c-c c-l + import

[gallais]

Hi Serge,

According to the wiki :
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary

=====================
Setting up the Emacs mode for use with the library

Download the library and unpack it into some directory DIR.
In Emacs, type the following commands:

   M-x load-library RET agda2-mode RET
   M-x customize-group RET agda2 RET

Look for the option Agda2 Include Dirs. Insert the path DIR/src.
Click Save for Future Sessions.
=====================

--
gallais


On 23 April 2013 19:24, Serge D. Mechveliani <mechvel at botik.ru> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130423/2a79d60a/attachment.html