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

[Guillaume Brunerie]

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-.

I'm using a not-so-recent build of Agda 2.3.3

Guillaume
Le 24 juil. 2013 15:51, "Francesco Mazzoli" <f at mazzo.li> a écrit :

> At Wed, 24 Jul 2013 14:41:29 +0200,
> Guillaume Brunerie wrote:
> > I'm confused. I just tried and x is visible in { }0 in both cases (and it
> > would be indeed very annoying if it wasn't the case, I use "where" quite
> > often (not so much "let"))
> > Could you give a reproducible test case?
>
> “let” and “where” are different.  “where” creates an additional
> top-level definition, as Darryl suggested, while “let” doesn’t (not sure
> if it desugars to something or it is a dedicated construct).
>
> For instance if you have
>
>     foo : forall {A : Set} -> A -> A
>     foo x = let y = x in {!!}
>
> “y” won’t show up in the goal (at least with my Agda, which is a fairly
> recent darcs build).
>
> Francesco
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130724/bd2037b3/attachment.html