[Agda] Insightful let's and where's

[Guillaume Brunerie]

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?

Guillaume
Le 24 juil. 2013 12:56, "Darryl McAdams" <psygnisfive at yahoo.com> a écrit :

> In code like
>
>     let x : A
>         x = ...
>     in { }0
>
> or
>
>     ... = { }0
>     where x : A
>               x = ...
>
> it would be enormously useful if x was visible in { }0, but of course this
> doesn't happen in Agda currently. Is there a deep reason why this is the
> case? I think I've read that let's and where's desugar to top-level
> definitions. it might then be useful to desugar not to top level defs in
> isolation, but to top-level defs + applications
>
>     let x : A
>         x = ...
>     in { }0
>
> becoming
>
>     aux_x : A
>     aux_x = ...
>
>     (\x -> { }0) aux_x
>
> or something like that.
>
> - darryl
>
> _______________________________________________
> 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/7a4a903b/attachment.html