[Agda] Re: Insightful let's and where's
Darryl McAdams
psygnisfive at yahoo.com
Mon Jul 29 00:30:03 CEST 2013
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-,
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:
foo x = (\y -> {! !}) x
which you can abstract out into a silly thing:
better-let : (A : Set) {B : Set} → (A → B) → A → B
better-let A f x = f x
syntax better-let A (λ x → y) z = better-let x :: A := z , y
which lets you now write
foo x = better-let y :: A := x , {! !}
but this is silly. lets and where's are very simple context extending things that ought to really be visible in their scopes.
- darryl
________________________________
From: Francesco Mazzoli <f at mazzo.li>
To: Guillaume Brunerie <guillaume.brunerie at gmail.com>
Cc: agda list <agda at lists.chalmers.se>
Sent: Wednesday, July 24, 2013 10:13 AM
Subject: Re: [Agda] Re: Insightful let's and where's
At Wed, 24 Jul 2013 16:09:28 +0200,
Guillaume Brunerie wrote:
> If I write the following:
>
> foo : forall {A : Set} -> A -> A
> foo x = let y = x in {! y !}
>
> 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:
>
> Goal: .A
> Have: .A
> -------------------
> x : .A
> .A : Set
>
> (in particular, y is recognized as something of type A)
> Moreover,
C-c C-space replaces the goal by y, as expected.
>
> So what do you mean by "y does not show up in the goal"?
> 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-.
Yep, I’m pretty sure that what Darryl was referring too was the fact
that “let”-bound variables do not show up in the context—I find myself
annoyed by that too, although as you say it is not essential.
Since the Emacs window is titled “*Goal type etc.*” I just call that
whole listing “goal”, but I agree that “context” is more accurate.
Francesco
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130728/48b8bc56/attachment.html
More information about the Agda
mailing list