<p dir="ltr">If I write the following:</p>
<p dir="ltr"> foo : forall {A : Set} -> A -> 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 "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 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'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, "Francesco Mazzoli" <<a href="mailto:f@mazzo.li">f@mazzo.li</a>> 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>
> I'm confused. I just tried and x is visible in { }0 in both cases (and it<br>
> would be indeed very annoying if it wasn't the case, I use "where" quite<br>
> often (not so much "let"))<br>
> 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} -> A -> 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>