<p dir="ltr">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"))<br>
Could you give a reproducible test case?</p>
<p dir="ltr">Guillaume</p>
<div class="gmail_quote">Le 24 juil. 2013 12:56, "Darryl McAdams" <<a href="mailto:psygnisfive@yahoo.com">psygnisfive@yahoo.com</a>> a écrit :<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div><div style="font-size:10pt;font-family:arial,helvetica,sans-serif"><div><span>In code like</span></div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif">
<span><br></span></div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif"><span> let x : A</span></div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif">
x = ...</div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif"> in { }0</div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif">
<br></div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif">or</div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif">
<br></div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif"> ... = { }0</div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif">
where x : A</div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif"> x = ...</div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif">
<br></div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif">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</div>
<div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif"><br></div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif">
<span style="background-color:transparent;font-size:10pt"> let x : A</span></div><div style="background-color:transparent"> x = ...</div><div style="background-color:transparent"> in { }0</div><div></div><div>
<br></div><div>becoming</div><div><br></div><div> aux_x : A</div><div> aux_x = ...</div><div><br></div><div> (\x -> { }0) aux_x</div><div><br></div><div>or something like that.</div><div> </div><div>- darryl</div>
</div></div><br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div>