Skip to content

feat: append iterator combinator#12844

Draft
datokrat wants to merge 1 commit intomasterfrom
paul/iter-append
Draft

feat: append iterator combinator#12844
datokrat wants to merge 1 commit intomasterfrom
paul/iter-append

Conversation

@datokrat
Copy link
Contributor

@datokrat datokrat commented Mar 9, 2026

This PR provides the iterator combinator append that permits the concatenation of two iterators.

@datokrat datokrat added the changelog-library Library label Mar 9, 2026
@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 Mar 9, 2026
@mathlib-lean-pr-testing
Copy link

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-07 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-09 11:13:26)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-07 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. (2026-03-09 11:13:28)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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.

2 participants