[Agda] interaction/repl when in agda-mode

[Jim Burton]

At Fri, 31 Oct 2008 17:59:22 +0100,
Ulf Norell wrote:
> 
> [1  <multipart/alternative (7bit)>]
> [1.1  <text/plain; UTF-8 (7bit)>]
> On Fri, Oct 31, 2008 at 5:56 PM, Jim Burton <jim at sdf-eu.org> wrote:
> 
> > Hi, I am playing with the examples in Ulf Norell's excellent tutorial,
> > and the only way I've found to do this is to have an emacs window in
> > agda-mode and one with `agda -I' running in it, and to switch between
> > windows reloading the module as I go. But I notice that running agda
> > like this isn't supported. Is there a better way of doing things
> > interactively?
> 
> 
> I'm glad you like the tutorial :-)
>

Hi Ulf, I do like the tutorial and I like Agda too -- being new to
dependent types I am averaging 2 "wow, can you do that?"s per page :-)
 
> 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.

Jim

> / Ulf
> [1.2  <text/html; UTF-8 (7bit)>]
> 
> [2  <text/plain; us-ascii (7bit)>]
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda