The Coq mailing list

[Noam Zeilberger <noam+coq AT cs.cmu.edu>]

This was supposed to go out before the previous mesage, but I
accidentally sent it with the wrong (non-list-member) address.
Anyways, thanks to Adam, Xavier, and Matthieu for their helpful
responses!  I might post another question about parameterized
mutually-inductive definitions soon...but I have to formulate
the question first.

Noam

On Wed, Aug 01, 2007 at 05:01:57PM -0400, Noam Zeilberger wrote:
> I was wondering if there is some sort of tutorial/FAQ for working with
> mutually-(co)inductive definitions in Coq?  I'm looking for something
> more than just the documentation of the Scheme command.  For example,
> what is the most natural way of taking an ordinary mathematical proof
> of a list of theorems by simultaneous induction, and encoding it in
> the tactic language?  Has anyone done any significant amount of
> theorem-proving using mutually-inductive definitions with more than
> (say) three branches?
> 
> Noam