coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mutual induction Schemes

From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>
To: Randy Pollack <rap AT dcs.ed.ac.uk>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Mutual induction Schemes
Date: Mon, 30 Sep 2002 23:38:36 +0200 (MEST)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Randy Pollack writes:
>
> What is the intended use of mutual induction schemes generated by
> "Scheme"? Are there tactics such as "NewInduction" to use them, or do
> we create the induction predicates by hand and use more basic tactics
> like "Apply"?

As far as I'm concerned, I always applied them manually using a
combination of Pattern and Apply.

--
Jean-Christophe

[Coq-Club] Mutual induction Schemes, Randy Pollack
- Re: [Coq-Club] Mutual induction Schemes, Jean-Christophe Filliatre