The Coq mailing list

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

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.