<p dir="ltr">I&#39;m confused. I just tried and x is visible in { }0 in both cases (and it would be indeed very annoying if it wasn&#39;t the case, I use &quot;where&quot; quite often (not so much &quot;let&quot;))<br>
Could you give a reproducible test case?</p>
<p dir="ltr">Guillaume</p>
<div class="gmail_quote">Le 24 juil. 2013 12:56, &quot;Darryl McAdams&quot; &lt;<a href="mailto:psygnisfive@yahoo.com">psygnisfive@yahoo.com</a>&gt; 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&#39;t happen in Agda currently. Is there a deep reason why this is the case? I think I&#39;ve read that let&#39;s and where&#39;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 -&gt; { }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>