[Agda] Agda goes coinductive

[Ulf Norell]

On Fri, Jun 6, 2008 at 3:35 AM, Dan Doel <dan.doel at gmail.com> wrote:

>
> > -- complaint: never != later never
>
>  map f (now v) != now (f v)
>
> Is this to be expected, or is it an oversight?
>

This is the expected behaviour. When checking equality it's not safe to
unfold corecursive functions. You can probably work around it by defining
unfolding functions to force the unfolding. For instance,

unfold : {a : Set} -> D a -> D a
unfold (now x) = now x
unfold (lated d) = later d

You have unfold (map f (now v)) == now (f v).

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080606/1d6ef226/attachment-0001.html