8000 feat: introduce slices by datokrat · Pull Request #8947 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

feat: introduce slices #8947

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 24 commits into from
Jun 26, 2025
Merged

feat: introduce slices #8947

merged 24 commits into from
Jun 26, 2025
+1,242 −499

Conversation

datokrat
Copy link
Contributor
@datokrat datokrat commented Jun 23, 2025 •
edited
Loading

This PR introduces polymorphic slices in their most basic form. They come with a notation similar to the new range notation. Subarray is now also a slice and can produce an iterator now. It is intended to migrate more operations of Subarray to the Slice wrapper type to make them available for slices of other types, too.

The PR also moves the filterMap combinators into Init because they are used internally to implement iterators on array slices.

@datokrat datokrat added the changelog-library Library label Jun 23, 2025
@datokrat datokrat force-pushed the paul/slices/introduce-slices branch from 433b4dd to b131e8a Compare June 24, 2025 19:07
@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 Jun 24, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 24, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8947
157b8d0
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jun 24, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8947
8e3551f
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 24, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#8947
a5ec4d8
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jun 24, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#8947
14b9014
@datokrat datokrat force-pushed the paul/base/slices/introduce-slices branch from 15482bc to ce1698d Compare June 25, 2025 08:23
@datokrat datokrat force-pushed the paul/slices/introduce-slices branch from 3496e27 to 48385b9 Compare June 25, 2025 08:23
@leanprover-community-bot
Copy link
Collaborator
leanprover-community-bot commented Jun 25, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-06-24 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-25 09:08:57)
    Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 40d2c9946319716228b414e501e71b7f959e1619 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. (2025-06-26 11:40:19)
  • 💥 Mathlib branch lean-pr-testing-8947 build failed against this PR. (2025-06-26 11:43:34) View Log
  • ✅ Mathlib branch lean-pr-testing-8947 has successfully built against this PR. (2025-06-26 15:22:53) View Log

@datokrat datokrat marked this pull request as ready for review June 25, 2025 09:13
@datokrat datokrat requested review from TwoFX and kim-em as code owners June 25, 2025 09:13
@datokrat datokrat marked this pull request as draft June 25, 2025 11:31
@datokrat datokrat marked this pull request as ready for review June 25, 2025 15:33
@datokrat
Copy link
Contributor Author
datokrat commented Jun 25, 2025 •
edited
Loading

@david-christiansen I think you are being notified because you are the code owner of Subarray. Here's some context: I am migrating Subarray to a more polymorphic setting. This required me to replace the definition of Subarray. However, I am keeping its whole public API except for low-level details (e.g. the constructor). Not many things broke besides Subarray.lean and Subarray/Split.lean
While fixing some compile errors in Split.lean, I also implemented split in terms of take and drop. Feel free to leave comments if you think that things could be improved!

@david-christiansen
Copy link
Contributor

It all looks good to me :)

@datokrat datokrat force-pushed the paul/slices/introduce-slices branch from f3b4e38 to 1c51792 Compare June 26, 2025 07:51
TwoFX
TwoFX reviewed Jun 26, 2025
View reviewed changes
10000
@datokrat datokrat force-pushed the paul/base/slices/introduce-slices branch from 320a364 to 40d2c99 Compare June 26, 2025 11:18
@datokrat datokrat force-pushed the paul/slices/introduce-slices branch from 1c51792 to 59e070c Compare June 26, 2025 11:18
@datokrat datokrat changed the base branch from paul/base/slices/introduce-slices to master June 26, 2025 11:19
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#8947
9072d15
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jun 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#8947
907b351
@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 Jun 26, 2025
@datokrat datokrat mentioned this pull request Jun 26, 2025
Merged
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#8947
e2b1041
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jun 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#8947
f17cb92
@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 Jun 26, 2025
@datokrat datokrat added this pull request to the merge queue Jun 26, 2025
Merged via the queue into master with commit 83e2262 Jun 26, 2025
28 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

@david-christiansen david-christiansen Awaiting requested review from david-christiansen david-christiansen is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library force-mathlib-ci 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.
4 participants
@datokrat @leanprover-community-bot @david-christiansen @TwoFX
0