coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Is there a way to access the induction principle of an inductive type from a type term?

From: <michael.soegtrop AT intel.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Is there a way to access the induction principle of an inductive type from a type term?
Date: Tue, 18 Nov 2014 13:04:30 +0100

Dear Coq users,

when I define an inductive type, a set of induction principles is created
automatically by Coq. When I have some term for an inductive type, is there a
way to access its default induction principles from the type term? I am
looking for somethign which works in the term language, not in the tactics
language.

Thanks & best regards,

Michael

[Coq-Club] Is there a way to access the induction principle of an inductive type from a type term?, michael.soegtrop, 11/18/2014
- Re: [Coq-Club] Is there a way to access the induction principle of an inductive type from a type term?, Adam Chlipala, 11/18/2014
  - Re: [Coq-Club] Is there a way to access the induction principle of an inductive type from a type term?, Jason Gross, 11/18/2014
  - Re: [Coq-Club] Is there a way to access the induction principle of an inductive type from a type term?, michael.soegtrop, 11/19/2014