[Agda] interactive evaluation and typechecking

[Ramana Kumar]

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.