<p dir="ltr">If I write the following:</p>
<p dir="ltr">    foo : forall {A : Set} -&gt; A -&gt; A<br>
    foo x = let y = x in {! y !}</p>
<p dir="ltr">Then C-c C-l to load the file and C-c C-. in the goal to get the type of the content of the goal and the type expected, I get:</p>
<p dir="ltr">    Goal: .A<br>
    Have: .A<br>
    -------------------<br>
    x : .A<br>
    .A : Set</p>
<p dir="ltr">(in particular, y is recognized as something of type A)<br>
Moreover, C-c C-space replaces the goal by y, as expected.</p>
<p dir="ltr">So what do you mean by &quot;y does not show up in the goal&quot;?<br>
Maybe you mean that it does not show up in the *context*, but I don&#39;t find that particularly annoying given that (at least for where) the type is written is full a few lines below anyway, and for let you can ask Agda the type of any term with C-c C-d or C-c C-.</p>

<p dir="ltr">I&#39;m using a not-so-recent build of Agda 2.3.3</p>
<p dir="ltr">Guillaume</p>
<div class="gmail_quote">Le 24 juil. 2013 15:51, &quot;Francesco Mazzoli&quot; &lt;<a href="mailto:f@mazzo.li">f@mazzo.li</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">
At Wed, 24 Jul 2013 14:41:29 +0200,<br>
Guillaume Brunerie wrote:<br>
&gt; I&#39;m confused. I just tried and x is visible in { }0 in both cases (and it<br>
&gt; would be indeed very annoying if it wasn&#39;t the case, I use &quot;where&quot; quite<br>
&gt; often (not so much &quot;let&quot;))<br>
&gt; Could you give a reproducible test case?<br>
<br>
“let” and “where” are different.  “where” creates an additional<br>
top-level definition, as Darryl suggested, while “let” doesn’t (not sure<br>
if it desugars to something or it is a dedicated construct).<br>
<br>
For instance if you have<br>
<br>
    foo : forall {A : Set} -&gt; A -&gt; A<br>
    foo x = let y = x in {!!}<br>
<br>
“y” won’t show up in the goal (at least with my Agda, which is a fairly<br>
recent darcs build).<br>
<br>
Francesco<br>
<br>
<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>
</blockquote></div>