[Agda] defining coinductive types

Wojciech Jedynak wjedynak at gmail.com
Wed Dec 18 18:14:22 CET 2013


> Ok, I see.  Is it known that supporting non-strictly positive types would
> have bad consequences in Agda?  Not that I am suggesting it -- I am just
> curious about what might be possible.

Yes, it's possible to write a non-terminating expression using such a
type. For instance, take a look here:


More information about the Agda mailing list