Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Need help with coinductive proof

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Need help with coinductive proof


chronological Thread 
  • From: Nils Anders Danielsson <nad AT Cs.Nott.AC.UK>
  • To: coq-club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Need help with coinductive proof
  • Date: Tue, 25 Aug 2009 22:35:44 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On 2009-08-25 14:22, Edsko de Vries wrote:
If there is a nicer way to achieve this I'd be interested to hear it.

Like Thorsten suggested you could try encoding a nested fixpoint
manually, using an inner Inductive declaration and an outer CoInductive
declaration.

how does Agda verify that your definition of fibP is correct?

A short answer: Agda accepts the definition you refer to because all
corecursive calls are guarded by constructors, at least one of which is
coinductive (♯_).

--
/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.





Archive powered by MhonArc 2.6.16.

Top of Page