Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Mutual induction with list

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mutual induction with list


Chronological Thread 
  • 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/




Archive powered by MHonArc 2.6.18.

Top of Page