Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] induction principle for mutual induction on non-mutually-defined types (Coq'Art 14.3.3)?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] induction principle for mutual induction on non-mutually-defined types (Coq'Art 14.3.3)?


chronological Thread 
  • From: Jim Apple <coq-club AT jbapple.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] induction principle for mutual induction on non-mutually-defined types (Coq'Art 14.3.3)?
  • Date: Thu, 2 Sep 2010 17:10:03 -0400
I forgot "apply ans" before the commented-out Guarded.

Also, I see the same behavior with 8.3-rc1.

Archive powered by MhonArc 2.6.16.

Top of Page