<div dir="ltr">Hi Serge,<br><br>According to the wiki :<br><a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary</a><br>
<br>=====================<br>Setting up the Emacs mode for use with the library<br><br>Download the library and unpack it into some directory DIR.<br>In Emacs, type the following commands:<br><br>š šM-x load-library RET agda2-mode RET<br>
š šM-x customize-group RET agda2 RET<br><br>Look for the option Agda2 Include Dirs. Insert the path DIR/src.<br>Click Save for Future Sessions.<div>=====================</div></div><div class="gmail_extra"><br clear="all">
<div>--<br>gallais</div>
<br><br><div class="gmail_quote">On 23 April 2013 19:24, Serge D. Mechveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
People,<br>
I am trying to use the Agda interactive environvent under Emacs,<br>
by following the instructions on šQuick Editing Guide šon the Web.<br>
I edit šT.agda šin šemacs, šwith using the Agda mode.<br>
If šT.agda šdoes not import the Library, then š c-c c-l šseems to<br>
type-check.<br>
But if šT.agda šuses something from Standard Library, then it reports<br>
something about the library module.<br>
<br>
On the other hand, šagda -c $agdaLibOpt T.agda<br>
<br>
does work in the command line.<br>
How to bring the library modules to the emacs interactive shell?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>