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

[Apostolis Xekoukoulotakis]

There is an issue already.


https://github.com/agda/agda/issues/888

On Sun, Apr 30, 2017 at 7:24 PM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> 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/f8dc322e/attachment.html>