<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>In code like</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span>&nbsp; &nbsp; let x : A</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">&nbsp; &nbsp; &nbsp; &nbsp; x = ...</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">&nbsp; &nbsp; in { }0</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif;
 background-color: transparent; font-style: normal; "><br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">or</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">&nbsp; &nbsp; ... = { }0</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">&nbsp; &nbsp; where x : A</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; x = ...</div><div style="color: rgb(0, 0, 0);
 font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">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="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span style="background-color: transparent; font-size:
 10pt; ">&nbsp; &nbsp; let x : A</span></div><div style="background-color: transparent; ">&nbsp; &nbsp; &nbsp; &nbsp; x = ...</div><div style="background-color: transparent; ">&nbsp; &nbsp; in { }0</div><div></div><div><br></div><div>becoming</div><div><br></div><div>&nbsp; &nbsp; aux_x : A</div><div>&nbsp; &nbsp; aux_x = ...</div><div><br></div><div>&nbsp; &nbsp; (\x -&gt; { }0) aux_x</div><div><br></div><div>or something like that.</div><div>&nbsp;</div><div>- darryl</div>  </div></body></html>