Skip to content

feat: add Array.partitionM, Array.partitionMapM, Array.partitionMap, List.partitionMapM #10215

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
Open
srghma wants to merge 2 commits into
base: master
Choose a base branch
from
Open

feat: add Array.partitionM, Array.partitionMapM, Array.partitionMap, List.partitionMapM #10215

srghma wants to merge 2 commits into from

Conversation

@srghma
Copy link

@srghma srghma commented Sep 2, 2025 •
edited
Loading

This PR adds Array.partitionM, Array.partitionMapM, Array.partitionMap, List.partitionMapM. Also it rewrites List.partitionMap to use List.partitionMapM

@srghma srghma force-pushed the feat-add-array-partitionM-and-others branch from ac2404f to 23d9c3a Compare September 2, 2025 11:28
@TwoFX TwoFX added the changelog-library Library label Sep 2, 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 Sep 2, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Sep 2, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-08-31 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-09-02 12:16:45)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 72ddc479bf038b6d94f12ae1dd08f28019be9712 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-06 01:57:30)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 2, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10215
6be0aff
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 2, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10215
df2e4a2
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Sep 2, 2025
@leanprover-community-bot
Copy link
Collaborator

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

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-10215 has successfully built against this PR. (2025-09-02 13:21:36) View Log
  • ✅ Mathlib branch lean-pr-testing-10215 has successfully built against this PR. (2025-09-03 01:30:06) View Log
  • ✅ Mathlib branch lean-pr-testing-10215 has successfully built against this PR. (2025-09-08 03:15:55) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 72ddc479bf038b6d94f12ae1dd08f28019be9712 --onto 455fd0b4488e2adc85f825a52e2ee7d944a5740a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-06 01:57:28)

eric-wieser
eric-wieser reviewed Sep 2, 2025
View reviewed changes
@srghma srghma force-pushed the feat-add-array-partitionM-and-others branch from 23d9c3a to 838194c Compare September 2, 2025 23:42
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 3, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10215
81c8c0a
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 3, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10215
9af80de
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Sep 4, 2025
@srghma srghma force-pushed the feat-add-array-partitionM-and-others branch from 838194c to d236cf8 Compare September 8, 2025 01:09
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 8, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10215
c680147
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 8, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10215
60a3cdd
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

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

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

1 more reviewer

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

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library P-medium We may work on this issue if we find the time 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

@srghma @leanprover-bot @leanprover-community-bot @eric-wieser @TwoFX