<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span style="font-size: 10pt; ">It's about what's visible in the context, not what's usable. Obviously let and where things are usable. But neither show up in the context when you do C-c C-,</span><br></div><div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "><div class="y_msg_container"><div id="yiv0823643373"><div style="color: rgb(0, 0, 0); background-color: rgb(255, 255, 255); font-family: arial, helvetica, sans-serif; font-size: 10pt; "><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; ">Notice, Guillaume, that you have x : .A, but not y : .A. This is acceptable in some situations, but not in others. It's often very useful to be able to write in a forward chaining style locally, and be able to see that you've done this without having to search through code. Note that you can obviously fake it using lambdas:</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; ">foo x = (\y -&gt; {! !}) 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; ">which you can abstract out into a silly thing:</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; "><div style="background-color:transparent;">&nbsp; &nbsp; better-let : (A : Set) {B : Set} → (A → B) → A → B</div><div style="background-color:transparent;">&nbsp; &nbsp; better-let A f x = f x</div><div style="background-color:transparent;">&nbsp; &nbsp;&nbsp;</div><div style="background-color:transparent;">&nbsp; &nbsp; syntax better-let A (λ x → y) z = better-let x :: A := z , y</div><div style="background-color:transparent;"><br></div><div style="background-color: transparent; color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif;
 font-style: normal; ">which lets you now write</div><div style="background-color: transparent; color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; font-style: normal; "><br></div><div style="background-color: transparent; color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; font-style: normal; ">foo x =
 better-let y :: A := x , {! !}</div><div style="background-color: transparent; color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; font-style: normal; "><br></div><div style="background-color: transparent; color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; font-style: normal; ">but this is silly. lets and where's are very simple context extending things that ought to really be visible in their scopes.</div></div><div></div><div>&nbsp;</div><div>- darryl<br></div>  <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "> <div dir="ltr"> <hr size="1">  <font size="2" face="Arial"> <b><span style="font-weight:bold;">From:</span></b> Francesco Mazzoli &lt;f@mazzo.li&gt;<br> <b><span style="font-weight:bold;">To:</span></b> Guillaume Brunerie &lt;guillaume.brunerie@gmail.com&gt; <br><b><span
 style="font-weight:bold;">Cc:</span></b> agda list &lt;agda@lists.chalmers.se&gt; <br> <b><span style="font-weight:bold;">Sent:</span></b> Wednesday, July 24, 2013 10:13 AM<br> <b><span style="font-weight:bold;">Subject:</span></b> Re: [Agda] Re: Insightful let's and where's<br> </font> </div> <div class="yiv0823643373y_msg_container"><br>At Wed, 24 Jul 2013 16:09:28 +0200,<br>Guillaume Brunerie wrote:<br>&gt; If I write the following:<br>&gt; <br>&gt;&nbsp; &nbsp;  foo : forall {A : Set} -&gt; A -&gt; A<br>&gt;&nbsp; &nbsp;  foo x = let y = x in {! y !}<br>&gt; <br>&gt; Then C-c C-l to load the file and C-c C-. in the goal to get the type of<br>&gt; the content of the goal and the type expected, I get:<br>&gt; <br>&gt;&nbsp; &nbsp;  Goal: .A<br>&gt;&nbsp; &nbsp;  Have: .A<br>&gt;&nbsp; &nbsp;  -------------------<br>&gt;&nbsp; &nbsp;  x : .A<br>&gt;&nbsp; &nbsp;  .A : Set<br>&gt; <br>&gt; (in particular, y is recognized as something of type A)<br>&gt;
 Moreover,
 C-c C-space replaces the goal by y, as expected.<br>&gt; <br>&gt; So what do you mean by "y does not show up in the goal"?<br>&gt; Maybe you mean that it does not show up in the *context*, but I don't find<br>&gt; that particularly annoying given that (at least for where) the type is<br>&gt; written is full a few lines below anyway, and for let you can ask Agda the<br>&gt; type of any term with C-c C-d or C-c C-.<br><br>Yep, I’m pretty sure that what Darryl was referring too was the fact<br>that “let”-bound variables do not show up in the context—I find myself<br>annoyed by that too, although as you say it is not essential.<br><br>Since the Emacs window is titled “*Goal type etc.*” I just call that<br>whole listing “goal”, but I agree that “context” is more accurate.<br><br>Francesco<br>_______________________________________________<br>Agda mailing list<br><a rel="nofollow" ymailto="mailto:Agda@lists.chalmers.se" target="_blank"
 href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br><a rel="nofollow" target="_blank" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br><br></div> </div> </div>  </div></div><br><br></div> </div> </div>  </div></body></html>