[Agda] interactive evaluation and typechecking

[Arseniy Alekseyev]

Hi Ramana.

Both of the things you've requested are available in Emacs Agda mode
together with a number of other useful commands.

You can query the type with C-c C-d.
You can normalize a term with C-c C-n.

A list of these and other key combinations can be found here:

http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.EmacsModeKeyCombinations

Cheers.
Arseniy.

On 14 November 2011 14:51, Ramana Kumar <rk436 at cam.ac.uk> wrote:
> I presume the only reasonable way to use Agda at the moment is via the
> emacs mode.
> I'd love to know if I'm wrong about that!
>
> Now, within the emacs mode, it seems like the only feedback available is
>  1. the whole buffer can be loaded and typechecks (or doesn't)
>  2. the type of some underscore (goal) ought to be <blah>
>
> Is there any facility for querying the type of a particular known term
> (as opposed to a goal)?
> (Similar to the "Check" command in Coq, for example.)
> Or for normalizing and showing a term (Like "Print" perhaps?)
> These things would help with, for example, knowing which identifier is
> in scope (when we haven't yet mastered Agda's scoping rules), but I
> imagine would also be useful for more interesting tasks.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>