lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

doc: adds missing docstrings related to iterators and ranges

Open david-christiansen opened this issue 1 month ago • 2 comments

This PR adds some missing docstrings for identifiers that appear in the manual and enables the missing documentation linter for their modules.

david-christiansen avatar Dec 09 '25 13:12 david-christiansen

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-community-bot avatar Dec 09 '25 15:12 leanprover-community-bot

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)

leanprover-bot avatar Dec 09 '25 15:12 leanprover-bot