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

[Francesco Mazzoli]

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