Skip to content

feat: ForIn, fold(M), drain lemmas for iterators #8405

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
wants to merge 5 commits into
base: paul/iterators/2-for-3
Choose a base branch
from
Open

feat: ForIn, fold(M), drain lemmas for iterators #8405

wants to merge 5 commits into from

Conversation

datokrat
Copy link
Contributor

This PR provides lemmas about the loop constructs ForIn, fold, foldM and drain and their relation to each other in the context of iterators.

@datokrat datokrat added the changelog-library Library label May 19, 2025
@datokrat datokrat changed the base branch from master to paul/iterators/2-for-3 May 19, 2025 12:25
@datokrat datokrat force-pushed the paul/iterators/3 branch from afe0983 to ba059db Compare May 20, 2025 08:31
@datokrat datokrat force-pushed the paul/iterators/2-for-3 branch from 4f37650 to 4df3d9b Compare May 20, 2025 08:31
@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 May 20, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 20, 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 60ea92fdb0594065072ed843724d98cd15b76fba --onto efe2ab4c04e81fe2a3edcc0d861449490b4431b2. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-20 09:00:05)
  • ✅ Mathlib branch lean-pr-testing-8405 has successfully built against this PR. (2025-05-20 17:31:10) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 96b81f3cc143d7925c68f4c0f50ff9628befc1e8 --onto 4eccb5b4792c270ad10ac059b9672a8845961079. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-23 14:41:41)

@datokrat datokrat force-pushed the paul/iterators/3 branch from ba059db to 5d96ec0 Compare May 20, 2025 12:45
@datokrat datokrat force-pushed the paul/iterators/2-for-3 branch from 4df3d9b to ec20d61 Compare May 20, 2025 12:45
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 20, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8405
18d3a54
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 20, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8405
5ab2b23
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label May 20, 2025
@datokrat datokrat marked this pull request as ready for review May 21, 2025 06:38
@datokrat datokrat requested a review from TwoFX as a code owner May 21, 2025 06:38
@datokrat datokrat force-pushed the paul/iterators/3 branch from 2ec8a83 to 096bf78 Compare May 23, 2025 14:02
@datokrat datokrat force-pushed the paul/iterators/2-for-3 branch from ec20d61 to 96b81f3 Compare May 23, 2025 14:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX 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.
2 participants
@datokrat @leanprover-community-bot