<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> 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; "> x = ...</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "> 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; "> ... = { }0</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "> 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; "> 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; "> 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></body></html>