coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Randy Pollack <rap AT dcs.ed.ac.uk>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Mutual induction Schemes
- Date: Mon, 30 Sep 2002 16:51:03 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello,
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"?
Best,
Randy
- [Coq-Club] Mutual induction Schemes, Randy Pollack
- Re: [Coq-Club] Mutual induction Schemes, Jean-Christophe Filliatre
Archive powered by MhonArc 2.6.16.