The Coq mailing list

[Nils Anders Danielsson <nad AT Cs.Nott.AC.UK>]

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.