[Agda] Re: [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not sound? (was: Need help with coinductive proof)

[Edsko de Vries]

On Tue, Sep 1, 2009 at 2:59 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk>wrote:

> It is sound but useless.
>

Then I clearly don't understand the rules for mixed inductive/coinductive
definitions. Is

   inductive_constructor (..) (coinductive_constructor (coinductive
recursive call))

a valid call or not?

Edsko
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090901/86fe81ed/attachment.html