8000 doc: review Repr and Format docstrings by david-christiansen · Pull Request #8998 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

doc: review Repr and Format docstrings #8998

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
merged 1 commit into from
Jun 26, 2025
Merged

doc: review Repr and Format docstrings #8998

merged 1 commit into from
Jun 26, 2025

Conversation

david-christiansen
Copy link
Contributor

This PR makes the docstrings related to Format and Repr have consistent formatting and style, and adds missing docstrings.

8000
@david-christiansen david-christiansen added documentation Documentation improvement changelog-doc Documentation labels Jun 25, 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 Jun 25, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-06-25 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. (2025-06-25 14:30:17)

@david-christiansen david-christiansen added the will-merge-soon …unless someone speaks up label Jun 25, 2025
@david-christiansen david-christiansen added this pull request to the merge queue Jun 26, 2025
Merged via the queue into leanprover:master with commit 5ec3cc5 Jun 26, 2025
27 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
changelog-doc Documentation documentation Documentation improvement toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@david-christiansen @leanprover-community-bot
0