coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to prove that inductive substructures are not equal?

From: Michiel Helvensteijn <mhelvens AT gmail.com>
To: Cedric Auger <sedrikov AT gmail.com>
Cc: Adam Chlipala <adamc AT csail.mit.edu>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How to prove that inductive substructures are not equal?
Date: Mon, 15 Jul 2013 20:04:06 +0200

On Mon, Jul 15, 2013 at 7:49 PM, Cedric Auger
<sedrikov AT gmail.com>
wrote:

> You can also take a look at "Induction Scheme" in the manual. I never use it
> personally, but I do not think either it is bad taste to use it.

Oooh. That might be the most massively useful tip I've gotten today. I
think "Combined Scheme" might be exactly what I've been looking for:

http://coq.inria.fr/distrib/current/refman/Reference-Manual015.html

Cheers!

--
www.mhelvens.net

[Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Adam Chlipala, 07/15/2013
  - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
  - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
    - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Adam Chlipala, 07/15/2013
      - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
      - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Cedric Auger, 07/15/2013
        
        Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
    - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Cedric Auger, 07/15/2013
      - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013