The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

If you were asking about the tactic language, then we could come up with Ltac wishlist items to pass on to the Coq team.  However, since you're asking about Gallina features, then let me say that I hope core Coq never supports any feature like you suggest, which would be a rather jarring departure from the parametricity features of the logic!

(See http://en.wikipedia.org/wiki/Parametricity .)

However, you can probably use type classes, which aren't part of the core formalized logic, to achieve the effect you're after.  I haven't worked out the details.

On 11/18/2014 07:04 AM, michael.soegtrop AT intel.com wrote:

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