[Agda] Some suggestions for the 'where' syntax and C-c C-,

[Apostolis Xekoukoulotakis]

Consider this example :

```
module test where


data T : Set where
  t : T
  tt : T

data D : T → Set where
  d : D t
  dt : D tt


f : T → T
f t = tt
f tt = t

g : (x : T) → D (f (f (f x)))
g x = {!!} where
 e = (f (f (f x)))

```

A. When someone checks the hole with C-c C-, , he does not see the type of
e.

B. It would be nice if the goal type and the context were updated to
contain the e variable.

If the expressions are very long, I currently have to check them very
carefully to see if the variable I have defined is the same as the
expression.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170430/d1f167ad/attachment-0001.html>