[Agda] Impossible proofs about where blocks?

[Daniel Peebles]

Oh! I had no idea this was even valid syntax. It's good to know, but yeah, I
guess the proof is impossible until the standard lib can be updated to use
this pattern?

Thanks,
Dan

On Thu, Jun 16, 2011 at 6:44 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

>
> On Thu, Jun 16, 2011 at 10:51 AM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:
>
>> In the back of my mind I remember from some Agda meeting talk that
>>
>>  bla : _
>>  bla = ...
>>    where blurp = ...
>>
>> allows one to access blurp as
>>
>>  bla.blurp
>>
>> But that does not seem to be the case...
>>
>> @Ulf:  Did such a feature exist at some time?
>>
>
> Yes, and it still does, but it requires that you name the where block.
>
> bla : _
> bla = ...
>   module BlaLocal where
>     blurp = ...
>
> let's you access blurp as BlaLocal.blurp. The reason you have to name it is
> that
> you can have several where blocks for the same definition (one for each
> clause),
> so it's not clear how to name them automatically.
>
> / Ulf
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110616/fed5ef9f/attachment.html