Skip to content
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

feat: Vector.getElem_flatMap #6661

Merged
merged 5 commits into from
Jan 16, 2025
Merged

feat: Vector.getElem_flatMap #6661

merged 5 commits into from
Jan 16, 2025

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Jan 16, 2025

This PR adds array indexing lemmas for Vector.flatMap. (These were not available for List and Array due to variable lengths.)

@kim-em kim-em added the changelog-library Library label Jan 16, 2025
@kim-em kim-em requested a review from digama0 as a code owner January 16, 2025 02:17
@kim-em kim-em marked this pull request as draft January 16, 2025 02:17
@kim-em
Copy link
Collaborator Author

kim-em commented Jan 16, 2025

To merge after #6660.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 16, 2025 02:31 Inactive
@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 Jan 16, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 16, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6259b4742c70d9621543ca4c4a086cbc6b6d55e0 --onto a955708b6c5f25e7f9c9ae7b951f8f3d5aefe377. (2025-01-16 02:39:22)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 80ddbf45eb92794b1df2cb625e9432753d41601b --onto a955708b6c5f25e7f9c9ae7b951f8f3d5aefe377. (2025-01-16 06:36:37)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 16, 2025 05:35 Inactive
@kim-em kim-em marked this pull request as ready for review January 16, 2025 06:12
@kim-em kim-em enabled auto-merge January 16, 2025 06:12
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 16, 2025 06:20 Inactive
@kim-em kim-em added this pull request to the merge queue Jan 16, 2025
Merged via the queue into master with commit f4c9934 Jan 16, 2025
16 checks passed
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Jan 21, 2025
@kim-em @luisacicolini
feat: Vector.getElem_flatMap (leanprover#6661)
528736d 
This PR adds array indexing lemmas for `Vector.flatMap`. (These were not
available for `List` and `Array` due to variable lengths.)
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
@kim-em @JovanGerb
feat: Vector.getElem_flatMap (leanprover#6661)
4381c34 
This PR adds array indexing lemmas for `Vector.flatMap`. (These were not
available for `List` and `Array` due to variable lengths.)
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

Assignees
No one assigned
Labels
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.
2 participants
@kim-em @leanprover-community-bot