[Coq-Club] Re: [Agda] Termination proof in partiality monad

[Vladimir Komendantsky]

2008/11/18 Luke Palmer <lrpalmer at gmail.com>

> Of course this will do it, because it is false!
>
> fac 3 = Later (Later (Later (Now 6)))
>
>
Okay. Then my earlier remark applies. Now what you can do is define an order
on [Delay A] and derive an equivalence relation "==" such that, for
instance, Later (Later (Later (Now 6))) == Now 6.

V
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081118/6aa723f7/attachment.html