[Agda] Re: Adding (inductive) transitivity to weak bisimilarity not sound?

[Nils Anders Danielsson]

On 2009-09-01 15:45, Edsko de Vries wrote:
> 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?

It is (currently, in Agda). I think you and Thorsten interpret the word
"sound" differently here.

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.