Skip to content

Conversation

@datokrat
Copy link
Contributor

@datokrat datokrat commented Dec 1, 2025

This PR moves many constants of the iterator API from Std.Iterators to the Std namespace in order to make them more convenient to use. These constants include, but are not limited to, Iter, IterM and IteratorLoop. This is a breaking change. If something breaks, try adding open Std. If some constants in Std.Iterators cannot be found, they can be found directly in Std now.

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

leanprover-bot commented Dec 2, 2025

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-01 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-12-02 09:56:30)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5339c47555cb65958259b1c4c4c687c3863a08be --onto 646df6ba16b3f68de539a085456c323e160e206d. You can force reference manual CI using the force-manual-ci label. (2025-12-13 00:29:14)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 2, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 2, 2025
@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 Dec 2, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 2, 2025

Mathlib CI status (docs):

  • 💥 Mathlib branch lean-pr-testing-11446 build failed against this PR. (2025-12-02 10:01:18) View Log
  • ✅ Mathlib branch lean-pr-testing-11446 has successfully built against this PR. (2025-12-02 20:06:02) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5339c47555cb65958259b1c4c4c687c3863a08be --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-13 00:29:13)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 2, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 2, 2025
@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 Dec 2, 2025
@datokrat datokrat closed this Dec 12, 2025
@datokrat datokrat force-pushed the paul/iterators/unnamespacing branch from decb095 to 19e1fe5 Compare December 12, 2025 15:11
@datokrat datokrat reopened this Dec 12, 2025
@datokrat datokrat force-pushed the paul/iterators/unnamespacing branch from fe9927a to 81a7772 Compare December 12, 2025 23:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

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

Development

Successfully merging this pull request may close these issues.

4 participants