[Agda] interactive evaluation and typechecking

[Wojciech Jedynak]

Hello,

2011/11/14 Ramana Kumar <rk436 at cam.ac.uk>:

> 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>

Note: underscores aren't called goals. Question marks are called goals.
Underscores mark terms that Agda should be able to infer using
unification, while question marks create goals (or sheds) that allow
all for all the interactive development features that Agda has.

All the thing you'd like to do can be done inside a goal (but not
only)- try C-c C-d and C-c C-n, for instance.
More details can be found at agda wiki:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode
and
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.EmacsModeKeyCombinations

To everybody: Ramana seems not to be the first person to think that _
should create goals. Is it because is it so in case of Coq (when using
refine)? I think we should make it more obvious for newcomers to Agda
that ? should be used.

Greetings,
W. Jedynak