Skip to content

Conversation

@datokrat
Copy link
Contributor

@datokrat datokrat commented Dec 4, 2025

This PR fixes a small oversight in a docstring.

@datokrat datokrat added the changelog-no Do not include this PR in the release changelog label Dec 4, 2025
@datokrat datokrat marked this pull request as ready for review December 4, 2025 16:47
@datokrat datokrat requested a review from kim-em as a code owner December 4, 2025 16:47
@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 4, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 4, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 4, 2025
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Dec 4, 2025
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Dec 4, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 4, 2025

Reference manual CI status:

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Dec 4, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@datokrat datokrat added this pull request to the merge queue Dec 5, 2025
Merged via the queue into master with commit f2415b7 Dec 5, 2025
33 checks passed
algebraic-dev pushed a commit that referenced this pull request Dec 8, 2025
This PR fixes a small oversight in a docstring.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

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-no Do not include this PR in the release changelog 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