lean4 feat: add option `tactic.customEliminators` to be able to turn off custom eliminators for `induction` and `cases`

feat: add option `tactic.customEliminators` to be able to turn off custom eliminators for `induction` and `cases`

Open kmill opened this issue 1 year ago • 1 comments

This was suggested by Scott Morrison to be able to help projects adjust to Nat having built-in custom eliminators.

Mar 12 '24 02:03 kmill

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-3655 build failed against this PR. (2024-03-12 03:17:12) View Log
✅ Mathlib branch lean-pr-testing-3655 has successfully built against this PR. (2024-03-28 02:28:36) View Log

Mar 12 '24 03:03 leanprover-community-mathlib4-bot

I think we can merge after resolving the conflict in RELEASES.md. It would be good to have this in 4.8.

Mar 25 '24 03:03 kim-em

@semorrison Updated

Mar 25 '24 04:03 kmill