[Agda] Insightful let's and where's

[Darryl McAdams]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130724/22ae5c03/attachment.html