The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Robin Green wrote:
> On Sat, 16 Feb 2008 22:14:46 -0500
> Robert Dockins 
> <robdockins AT fastmail.fm>
>  wrote:
>   
> >  It's pretty
> > counterintuitive to me that Coq is willing to look "through" a
> > previously defined function to discover properly formed recursive
> > calls but not through a function defined by mutual recursion.
> >     
>
> I'd imagine this is because two or more functions defined together by
> mutual recursion have to be both accepted as valid (including
> terminating) before either of them can be accepted as valid (if you
> see what I mean); thus, Coq won't unfold one of them in checking the
> other.
>   
Actually, my experience differs: mutual recursive definitions work only 
when the inductive types
that serve as main structure for the functions were defined 
simultaneously in a mutual inductive
definition.  It is not the case here: list and prod were defined before 
ex1.  So it is not a matter of
accepting to look through a function or not.

Yves