[Agda] interaction/repl when in agda-mode

[Ulf Norell]

On Fri, Oct 31, 2008 at 7:09 PM, Jim Burton <jim at sdf-eu.org> wrote:

>
> > Just using the emacs agda-mode should be enough. What is it you use "agda
> > -I" for?
>
> In order to use the repl -- so I enter some of your definitions and
> want to try executing the functions with some values. I couldn't find a
> command in agda-mode to do that.


Compute normal form (C-c C-n) does the same thing as just typing a term in
agda -I

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081031/8c6f7c51/attachment.html