coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: S3 <scubed2 AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Mutual induction with list
- Date: Sun, 20 May 2012 06:55:08 -0400
S3 wrote:
How do you have induction over a data structure
that contains a list?
This is a genuine Frequently Asked Question, and it's addressed in Section 3.8 of CPDT:
http://adam.chlipala.net/cpdt/
- [Coq-Club] Mutual induction with list, S3, 05/20/2012
- Re: [Coq-Club] Mutual induction with list, Adam Chlipala, 05/20/2012
- Re: [Coq-Club] Mutual induction with list, S3, 05/20/2012
- Re: [Coq-Club] Mutual induction with list, S3, 05/21/2012
- Re: [Coq-Club] Mutual induction with list, Frédéric Besson, 05/21/2012
- Re: [Coq-Club] Mutual induction with list, S3, 05/20/2012
- Re: [Coq-Club] Mutual induction with list, Adam Chlipala, 05/20/2012
Archive powered by MHonArc 2.6.18.