Skip to content

chore: deprecate variants other than inductive ... where #5533

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

chore: deprecate variants other than inductive ... where #5533

wants to merge 1 commit into from

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Sep 30, 2024 •
edited
Loading

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

@kmill
chore: deprecate variants other than inductive ... where
11e0fff 
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 leanprover#5236
@kmill kmill mentioned this pull request Sep 30, 2024
Open
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 30, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 30, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5533
94c484b
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 30, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5533
0478b9d
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Sep 30, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@david-christiansen
Copy link
Contributor

Out of curiosity, why should where be optional in the case of no constructors, rather than making it either mandatory or forbidden?

@david-christiansen
Copy link
Contributor

(where of course "forbidden" means "deprecated for a long long time" in this context)

@digama0
Copy link
Collaborator

digama0 commented Sep 30, 2024

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 where looks 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.

@david-christiansen
Copy link
Contributor

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!

@Thermotronica
Copy link

Aw man

eric-wieser
eric-wieser reviewed Oct 2, 2024
View reviewed changes
src/Init/Data/AC.lean
Comment on lines +12 to 13
inductive Expr where
| var (x : Nat)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In #5236 I thought the argument was leaning towards banning where for consistency with pattern-matched defs.

On the other hand, I guess match _ with | is already inconsistent when compared to inductive _ where | and def _ : _ |...

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@eric-wieser

In #5236 I thought the argument was leaning towards banning where for consistency with pattern-matched defs.

I believe this PR has been superseded by #5542 for approximately this reason.

@kmill kmill marked this pull request as draft October 8, 2024 22:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX is a code owner

@digama0 digama0 Awaiting requested review from digama0 digama0 is a code owner

@Vtec234 Vtec234 Awaiting requested review from Vtec234 Vtec234 is a code owner

@mhuisi mhuisi Awaiting requested review from mhuisi mhuisi is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

@tydeu tydeu Awaiting requested review from tydeu tydeu is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

Assignees
No one assigned
Labels
breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Deprecate and remove inductive ... :=
7 participants
@kmill @leanprover-community-bot @david-christiansen @digama0 @Thermotronica @eric-wieser @tydeu