<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 -> {! !}) 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;"> better-let : (A : Set) {B : Set} → (A → B) → A → B</div><div style="background-color:transparent;"> better-let A f x = f x</div><div style="background-color:transparent;"> </div><div style="background-color:transparent;"> 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> </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 <f@mazzo.li><br> <b><span style="font-weight:bold;">To:</span></b> Guillaume Brunerie <guillaume.brunerie@gmail.com> <br><b><span
style="font-weight:bold;">Cc:</span></b> agda list <agda@lists.chalmers.se> <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>> If I write the following:<br>> <br>> foo : forall {A : Set} -> A -> A<br>> foo x = let y = x in {! y !}<br>> <br>> Then C-c C-l to load the file and C-c C-. in the goal to get the type of<br>> the content of the goal and the type expected, I get:<br>> <br>> Goal: .A<br>> Have: .A<br>> -------------------<br>> x : .A<br>> .A : Set<br>> <br>> (in particular, y is recognized as something of type A)<br>>
Moreover,
C-c C-space replaces the goal by y, as expected.<br>> <br>> So what do you mean by "y does not show up in the goal"?<br>> Maybe you mean that it does not show up in the *context*, but I don't find<br>> that particularly annoying given that (at least for where) the type is<br>> written is full a few lines below anyway, and for let you can ask Agda the<br>> 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>