Skip to content

refactor: improve naming in the range API #10537

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
Merged
merged 6 commits into from
Oct 6, 2025
Merged

refactor: improve naming in the range API #10537

merged 6 commits into from
Oct 6, 2025

Conversation

datokrat
Copy link
Contributor

@datokrat datokrat commented Sep 24, 2025 •
edited
Loading

This PR renames some declarations in the range API for better consistency and readability. For example, UpwardEnumerable.succMany?_succ? is now called succMany?_add_one, in order to (a) correct the erroneous use of succ? instead of succ (=Nat.succ) and (b) distinguish the successor of natural numbers (add_one) from the successor of the upward-enumerable type (succ? or succ).

@datokrat datokrat force-pushed the paul/ranges/improvements branch from a4b93b8 to 501b1fa Compare October 2, 2025 06:54
@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 Oct 2, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 2, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-02 08:01:15)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 24c86fc05d5abeb147be04275fe6945d39f6b8c3 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-02 13:08:15)
  • ✅ Reference manual branch lean-pr-testing-10537 has successfully built against this PR. (2025-10-06 17:14:16) View Log
  • 🟡 Reference manual branch lean-pr-testing-10537 build against this PR didn't complete normally. (2025-10-06 17:14:25) View Log

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 2, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10537
c23c3ab
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 2, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10537
f37d236
@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 Oct 2, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 2, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❌ Mathlib branch lean-pr-testing-10537 built against this PR, but testing failed. (2025-10-02 09:02:03) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 24c86fc05d5abeb147be04275fe6945d39f6b8c3 --onto d88e417cda0f7afb1e15c806c6bfdbbb09ba7eef. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-02 13:08:14)
  • ✅ Mathlib branch lean-pr-testing-10537 has successfully built against this PR. (2025-10-06 18:30:14) View Log

@datokrat datokrat force-pushed the paul/ranges/improvements branch from 501b1fa to 79f4871 Compare October 2, 2025 12:13
@datokrat datokrat changed the base branch from paul/base/ranges/improvements to master October 2, 2025 12:13
@datokrat datokrat changed the title refactor: range API improvements refactor: improve naming in the range API Oct 2, 2025
@datokrat datokrat marked this pull request as ready for review October 2, 2025 12:57
@datokrat datokrat force-pushed the paul/ranges/improvements branch from 79f4871 to a813412 Compare October 6, 2025 16:08
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 6, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10537
89cbcb9
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Oct 6, 2025
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#10537
32a37ad
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 6, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10537
9c566e3
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Oct 6, 2025
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Oct 6, 2025
@datokrat datokrat added this pull request to the merge queue Oct 6, 2025
Merged via the queue into master with commit 7771b80 Oct 6, 2025
30 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR 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.

3 participants

@datokrat @leanprover-bot @leanprover-community-bot