[Agda] Re: type of identifier

[Francesco Mazzoli]

At Sat, 04 May 2013 11:45:58 +0400,
Sergei Meshveliani wrote:
> Please, how to show the type of an identifier in the interactive
> editing?
> I expected something like  "position cursor, C-c C-t",  
> but do not find.

Almost, you need ‘C-c C-d’, e.g. if I have

    foo : (A : Set) → A → A
    foo A x = {!!}

and I put my cursor in the goal, ‘C-c C-d A’ and ‘C-c C-d x’ deliver
expected results.

Francesco