Skip to content

refactor: replace Iter(M).size with Iter(M).count #10952

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
datokrat merged 11 commits into from
Nov 12, 2025
Merged

refactor: replace Iter(M).size with Iter(M).count #10952

datokrat merged 11 commits into from
Nov 12, 2025

Conversation

@datokrat
Copy link
Contributor

@datokrat datokrat commented Oct 25, 2025 •
edited
Loading

This PR replaces Iter(M).size with the Iter(M).count. While the former used a special IteratorSize type class, the latter relies on IteratorLoop. The IteratorSize class is deprecated. The PR also renames lemmas about ranges be replacing _Rcc with _rcc, _Rco with _roo (and so on) in names, in order to be more consistent with the naming convention.

@datokrat datokrat added the changelog-library Library label Oct 25, 2025
@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 25, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 25, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-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-25 08:53:38)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-10 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-11-12 12:07:02)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 25, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10952
1ec6ae4
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 25, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10952
8656ce9
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 25, 2025
@leanprover-community-bot
Copy link
Collaborator

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

Mathlib CI status (docs):

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 29, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10952
a642ac9
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 29, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10952
9f0be51
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 29, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10952
18678d8
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 29, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10952
ff1cc1f
@datokrat datokrat changed the title feat: size refactor: replace Iter(M).size with Iter(M).count Oct 30, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 30, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10952
24343ee
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 30, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10952
40ae982
@datokrat datokrat marked this pull request as ready for review October 30, 2025 08:58
@datokrat datokrat requested review from TwoFX and kim-em as code owners October 30, 2025 08:58
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 30, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10952
0d46451
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 30, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10952
ed54607
@leanprover-community-bot leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Oct 30, 2025
TwoFX
TwoFX reviewed Oct 31, 2025
View reviewed changes
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 31, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10952
67bda72
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 31, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10952
529c94b
@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 Nov 11, 2025
@datokrat datokrat force-pushed the paul/iterators/size branch from ad0cb28 to 92ff9e5 Compare November 12, 2025 11:20
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 12, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10952
d88353c
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Nov 12, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10952
687ea55
@datokrat datokrat added this pull request to the merge queue Nov 12, 2025
Merged via the queue into master with commit 9a3fb90 Nov 12, 2025
17 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX TwoFX left review comments

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library 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.

5 participants

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