coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Need help with coinductive proof, Edsko de Vries
- Re: [Coq-Club] Need help with coinductive proof,
Nils Anders Danielsson
- Re: [Coq-Club] Need help with coinductive proof,
Edsko de Vries
- Re: [Coq-Club] Need help with coinductive proof, Nils Anders Danielsson
- Re: [Coq-Club] Need help with coinductive proof,
Edsko de Vries
- Re: [Coq-Club] Need help with coinductive proof, Keiko Nakata
- Message not available
- Message not available
- Message not available
- Message not available
- Re: [Coq-Club] Need help with coinductive proof,
Thorsten Altenkirch
- Re: [Coq-Club] Need help with coinductive proof,
Thorsten Altenkirch
- [Coq-Club] Re: Need help with coinductive proof, Nils Anders Danielsson
- Re: [Coq-Club] Re: Need help with coinductive proof, Keiko Nakata
- Re: [Coq-Club] Re: Need help with coinductive proof, Keiko Nakata
- Re: [Coq-Club] Re: Need help with coinductive proof, Edsko de Vries
- Re: [Coq-Club] Need help with coinductive proof,
Thorsten Altenkirch
- Re: [Coq-Club] Need help with coinductive proof,
Thorsten Altenkirch
- Re: [Coq-Club] Need help with coinductive proof,
Edsko de Vries
- Re: [Coq-Club] Need help with coinductive proof, Thorsten Altenkirch
- Re: [Coq-Club] Need help with coinductive proof, Edsko de Vries
- Message not available
- Message not available
- Message not available
- Re: [Coq-Club] Need help with coinductive proof,
Nils Anders Danielsson
Archive powered by MhonArc 2.6.16.