[Agda] Insightful let's and where's
Darryl McAdams
psygnisfive at yahoo.com
Wed Jul 24 12:56:54 CEST 2013
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
More information about the Agda
mailing list