Skip to content

doc: adds missing docstrings related to iterators and ranges #11563

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
david-christiansen wants to merge 1 commit into
base: master
Choose a base branch
from
Open

doc: adds missing docstrings related to iterators and ranges #11563

david-christiansen wants to merge 1 commit into from
+45 −0

Conversation

@david-christiansen
Copy link
Contributor

@david-christiansen david-christiansen commented Dec 9, 2025

This PR adds some missing docstrings for identifiers that appear in the manual and enables the missing documentation linter for their modules.
@david-christiansen
doc: adds missing docstrings related to iterators and ranges
38e8209 
This PR adds some missing docstrings for identifiers that appear in the manual and enables the missing documentation linter for their modules.
@david-christiansen david-christiansen added the changelog-doc Documentation label Dec 9, 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 9, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 9, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bf51e1dcfa3322f639cb17e283a9b8caa1c16209 --onto 1d0d3915ca79d0875a757fc5061121ae9cd58543. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-09 15:08:11)
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 9, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bf51e1dcfa3322f639cb17e283a9b8caa1c16209 --onto 62f2f9229356039356c0469a46d8ecd77be88e2a. You can force reference manual CI using the force-manual-ci label. (2025-12-09 15:08:12)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-doc Documentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

3 participants

@david-christiansen @leanprover-community-bot @leanprover-bot