The example in the manual doesn't show the difference between the Induction and Elimination principles generated by Scheme.

I also imagined the Elimination principle would have type `forall P : Nat -> Set, P z -> (forall n : Nat, P (s n)) -> forall n : Nat, P n`

instead of the same one as the Induction Principle.

Why are they in fact the same ?

It seems Elimination and Case are the same as Induction and Minimality respectively except for naming, and have been that way since they were introduced in https://github.com/coq/coq/commit/ba360bdefa2d7e4200c94a37c5065019718c2691

Last updated: Jun 15 2024 at 05:01 UTC