The Coq mailing list

["shepi42 ." <fabian.pijcke AT gmail.com>]

Aww I'm sorry, I implemented my own _induction_ principle this morning, and I went wrong speaking about induction instead of inversion.

If I'm right, Print ind_nat prints out the induction principle generated by default, so my (real) question is "is there an equivalent command to print the inversion principle generated by default ?"

I've seen something like "Derive Inversion_clear", but I don't really get how this works and I'm not sure it correspond to the default inversion principle, especially, it seems trivially false cases are not wiped out.

Thank you for your answer anyway, just slap me twice if the inversion and induction principles use the same definition in definitive :p

Fabian Pijcke

2014-07-23 20:19 GMT+02:00 Jonathan <jonikelee AT gmail.com>:

On 07/23/2014 02:15 PM, Fabian Pijcke wrote:

Dear list,

I use the tactic "inversion H using myinversionprinciple.".

However, the principle I come with has several flaws. For example, it does not
introduce new variables automatically, and doesn't skip the trivially false
cases.

Is there a way to Check the default induction principle used for an Inductive
type ?

You mean, just to examine an existing one to see how it is defined? Try:  Print nat_ind.

-- Jonathan