The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Mutual recursion is easy to support via a single function whose domain 
is an inductive type, with each constructor carrying a tuple of the 
arguments that would go to one of the "mutually recursive" functions.  
You can define well-founded relations on inductive types like this.

On 07/14/2013 07:49 PM, Michiel Helvensteijn wrote:
> On Mon, Jul 15, 2013 at 1:00 AM, t 
> x<txrev319 AT gmail.com>
>   wrote:
>
>    
> > Note: I don't actually understand this technique and find "Function" with
> > "measure" much easier, but I think
> >
> > http://adam.chlipala.net/cpdt/html/GeneralRec.html
> >
> > is what you want.
> >      
> Thanks!
>
> I don't believe those techniques support mutually recursive functions
> either, so I'll still need an extra argument. But decreasing on a
> proof of relation well-foundedness, supported by the library, seems a
> great deal more elegant than my natural number idea.
>