Stream: Coq users

Topic: Difference between Induction and Elimination Schemes


view this post on Zulip Yann Leray (Jan 25 2023 at 12:19):

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 ?

view this post on Zulip Gaëtan Gilbert (Jan 25 2023 at 12:33):

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