Yann Leray (Jan 25 2023 at 12:19): 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 ?
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: Oct 13 2024 at 01:02 UTC