[Agda] Re: Insightful let's and where's

Francesco Mazzoli f at mazzo.li
Wed Jul 24 16:13:58 CEST 2013

At Wed, 24 Jul 2013 16:09:28 +0200,
Guillaume Brunerie wrote:
> If I write the following:
>     foo : forall {A : Set} -> A -> A
>     foo x = let y = x in {! y !}
> Then C-c C-l to load the file and C-c C-. in the goal to get the type of
> the content of the goal and the type expected, I get:
>     Goal: .A
>     Have: .A
>     -------------------
>     x : .A
>     .A : Set
> (in particular, y is recognized as something of type A)
> Moreover, C-c C-space replaces the goal by y, as expected.
> So what do you mean by "y does not show up in the goal"?
> Maybe you mean that it does not show up in the *context*, but I don't find
> that particularly annoying given that (at least for where) the type is
> written is full a few lines below anyway, and for let you can ask Agda the
> type of any term with C-c C-d or C-c C-.

Yep, I’m pretty sure that what Darryl was referring too was the fact
that “let”-bound variables do not show up in the context―I find myself
annoyed by that too, although as you say it is not essential.

Since the Emacs window is titled “*Goal type etc.*” I just call that
whole listing “goal”, but I agree that “context” is more accurate.


More information about the Agda mailing list