Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: Edsko de Vries <edskodevries AT gmail.com>
  • To: Thorsten Altenkirch <txa AT cs.nott.ac.uk>
  • Cc: Nils Anders Danielsson <nad AT cs.nott.ac.uk>, Agda list <agda AT lists.chalmers.se>, Coq Club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Agda] Re: [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not sound? (was: Need help with coinductive proof)
  • Date: Tue, 1 Sep 2009 15:45:10 +0100
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=ZFTvqhtJosmte+5vBvDz7nUMUk3ZUKay2At+kqyzW9lvBH3HQixfRh7JLGlDv5Q7Eo cGvLPacm1tFBjlpkdOJwMvT5lPivcpPR0nHridTGt/VTU07HOoIRw1yZWjUvEKf5IG7X K/ivAPP6dlQcX0H24y1gwT95cGVRzmttRSt8o=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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


Archive powered by MhonArc 2.6.16.

Top of Page