Skip to content

doc: add missing docstrings to iterator library #11912

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
david-christiansen merged 4 commits into from
Jan 8, 2026
Merged

doc: add missing docstrings to iterator library #11912

david-christiansen merged 4 commits into from
Jan 8, 2026
+97 −15

Conversation

@david-christiansen
Copy link
Contributor

@david-christiansen david-christiansen commented Jan 6, 2026

This PR adds missing docstrings for parts of the iterator library, which removes warnings and empty content in the manual.

@david-christiansen
doc: add missing docstrings to iterator library
1faab77 
This removes warnings when building the manual.
@david-christiansen david-christiansen added the changelog-doc Documentation label Jan 6, 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 Jan 6, 2026
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 6, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11912
25f1aa0
@github-actions github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Jan 6, 2026
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 6, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11912
659c52a
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 6, 2026
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#11912
805cabc
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Jan 6, 2026
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jan 6, 2026 •
edited
Loading

Reference manual CI status:

Rob23oba
Rob23oba previously requested changes Jan 6, 2026
View reviewed changes
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jan 6, 2026
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 6, 2026 •
edited
Loading

Mathlib CI status (docs):

@david-christiansen david-christiansen dismissed Rob23oba’s stale review January 6, 2026 16:35

The changes were implemented. Thanks!

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 6, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11912
c639ab1
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 6, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11912
b6ae965
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 6, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#11912
cf37405
datokrat
datokrat approved these changes Jan 7, 2026
View reviewed changes
Copy link
Contributor

@datokrat datokrat left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks a lot!

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 7, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11912
f4728c1
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 7, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11912
29f82d4
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 7, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#11912
e2eedde
@david-christiansen david-christiansen added this pull request to the merge queue Jan 8, 2026
Merged via the queue into leanprover:master with commit 7d5a969 Jan 8, 2026
18 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@datokrat datokrat datokrat approved these changes

+1 more reviewer

@Rob23oba Rob23oba Rob23oba left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-doc Documentation mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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.

5 participants

@david-christiansen @leanprover-bot @leanprover-community-bot @datokrat @Rob23oba