leanprover
chore: deprecate variants other than `inductive ... where`
Current state: This is a draft since there are some questions about whether no-where should be disallowed. #5542 deprecates just the := variant.
Deprecates inductive ... :=. Also, makes where required if there is at least one constructor. Currently produces a warning, controlled by linter.deprecated.
We don't require where when there are no constructors.
Closes #5236
Mathlib CI status (docs):
- 💥 Mathlib branch lean-pr-testing-5533 build failed against this PR. (2024-09-30 05:11:21) View Log
Out of curiosity, why should where be optional in the case of no constructors, rather than making it either mandatory or forbidden?
(where of course "forbidden" means "deprecated for a long long time" in this context)
I think having it be optional is defensible:
- It should be allowed to be omitted because there is a legitimate aesthetic/readability argument against it (
inductive Foo wherelooks like an unfinished sentence) - It should be allowed to be included because it is more regular (it makes editing easier if lists of 0+ things can be added or removed without requiring surrounding edits as well)
That is, downstream style guides could go either way on this, and we shouldn't try to fight with either option.
My concern here is only making the language surface area smaller, making it easier to learn the whole thing.
An optional where on constructorless types is not a huge increase.
Though I do disagree about downstream style guides - "the fewer style guides, the better" is an important lesson that Go taught us!
