[Agda] Agda's copatterns incompatible with initial algebras

[Dmitriy Traytel]

So I was just one day late.  Good to know that this issue worked on.

Thanks for the pointer, Andrea. Next time I'll check the bug tracker first.

Cheers,
Dmitriy

Am 19.06.2014 10:57, schrieb Andrea Vezzosi:
> Hi Dmitriy,
>
> Indeed there is a bug here [1] about sizes, you shouldn't be able to define
>
> shd wit = inn wit
>
> because inn requires the result size to increase.
>
> Cheers,
> Andrea
>
> [1] https://code.google.com/p/agda/issues/detail?id=1201
>
> On Wed, Jun 18, 2014 at 9:07 PM, Dmitriy Traytel <traytel at in.tum.de> wrote:
>> Dear Agda developers,
>>
>> today, I was able to prove false in Agda using copatterns and sized types
>> only (attached). Is my assumption, that those two extensions are supposed to
>> work together properly, correct?
>>
>> Especially, the definition of "wit" that refers to itself in order to
>> produce its own head looks fishy. I would have expected that something would
>> prevent me from doing this.
>>
>> This is my first proof in Agda, so please apologize if the example is not as
>> simplified as possible. The proof (and this email's title) is based on the
>> examples that exhibit the incompatibility of sized types and the "musical
>> coinduction" from [1] (of course replacing the "musical coinduction" by
>> copatterns).
>>
>> Or am I doing something completely wrong?
>>
>> Cheers,
>> Dmitriy
>>
>> [1] https://lists.chalmers.se/pipermail/agda/2011/003337.html
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>