The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

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