The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

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.

Cheers!

--
www.mhelvens.net