coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Noam Zeilberger <noam+ AT cs.cmu.edu>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] dealing with mutually-inductive definitions
- Date: Wed, 1 Aug 2007 17:01:57 -0400
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] dealing with mutually-inductive definitions, Noam Zeilberger
- Re: [Coq-Club] dealing with mutually-inductive definitions, Noam Zeilberger
- <Possible follow-ups>
- [Coq-Club] dealing with mutually-inductive definitions,
Noam Zeilberger
- Re: [Coq-Club] dealing with mutually-inductive definitions, Adam Chlipala
- Re: [Coq-Club] dealing with mutually-inductive definitions, Xavier Leroy
- Re: [Coq-Club] dealing with mutually-inductive definitions, Matthieu . Sozeau
- Re: [Coq-Club] dealing with mutually-inductive definitions, Matthieu . Sozeau
Archive powered by MhonArc 2.6.16.