Skip to content

style: fix doubled word in Lake docstring #11867

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

style: fix doubled word in Lake docstring #11867

alok wants to merge 1 commit into from
+13 −13

Conversation

@alok
Copy link
Contributor

@alok alok commented Jan 1, 2026

Summary

  • Fix "is not not" → "is not" in setupFile docstring

🤖 Generated with Claude Code

@alok @claude
style: fix typos in Lake docstrings and comments
2cf2e36 
This PR fixes various typos in Lake:

- Lake/CLI/Serve.lean: "not not" → "not"
- Lake/Build/Infos.lean: "obiligation" → "obligation" (6 occurrences)
- Lake/Load/Lean/Elab.lean: "a exclusive" → "an exclusive"
- Lake/Load/Lean/Elab.lean: "one the" → "on the"
- Lake/DSL/Syntax.lean: "located a fixed" → "located at a fixed"
- Lake/Config/Dependency.lean: "located a fixed" → "located at a fixed"
- Lake/CLI/Help.lean: "a archive" → "an archive" (2 occurrences)

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <[email protected]>
@alok alok force-pushed the typo/lake-doubled-words branch from 5791643 to 2cf2e36 Compare January 2, 2026 00:08
@alok alok marked this pull request as ready for review January 2, 2026 00:22
@alok alok requested a review from tydeu as a code owner January 2, 2026 00:22
@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 2, 2026
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 2, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ef9777ec0d03136128d5d998a2894a6ef38828b5 --onto c0d5e8bc2c925bc2b60f18c929acf7d73ea9ecec. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-02 01:08:38)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jan 2, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ef9777ec0d03136128d5d998a2894a6ef38828b5 --onto 9b1b932242309e0286882fc4ef2b5e02034aa405. You can force reference manual CI using the force-manual-ci label. (2026-01-02 01:08:40)

@tydeu
Copy link
Member

tydeu commented Jan 5, 2026

Thank you for fixing these typos! As this does more than just fix the doubled word, could you update the title and description of this PR to reflect this?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tydeu tydeu Awaiting requested review from tydeu tydeu is a code owner

Assignees

No one assigned

Labels

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.

4 participants

@alok @leanprover-community-bot @leanprover-bot @tydeu