Skip to content

chore: fix spelling #11531

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
nomeata merged 2 commits into from
Dec 6, 2025
Merged

chore: fix spelling #11531

nomeata merged 2 commits into from
Dec 6, 2025

Conversation

@tom93
Copy link
Contributor

@tom93 tom93 commented Dec 6, 2025

Hi, these are just some spelling corrections.

There is one I wasn't completely sure about in src/Init/Data/List/Lemmas.lean:

See also
...
Also
* `Init.Data.List.Monadic` for addiation (additional?) lemmas about `List.mapM` and `List.forM`

@nomeata
Copy link
Collaborator

nomeata commented Dec 6, 2025

Thanks! additional would be right, please add that fix and then I'll merge

@tom93
Copy link
Contributor Author

tom93 commented Dec 6, 2025 via email

@nomeata nomeata added this pull request to the merge queue Dec 6, 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 6, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 6, 2025

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-12-06 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-12-06 14:03:20)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 6, 2025

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-06 14:03:22)

Merged via the queue into leanprover:master with commit 2ca3bc2 Dec 6, 2025
16 checks passed
algebraic-dev pushed a commit that referenced this pull request Dec 8, 2025
@tom93 @algebraic-dev
chore: fix spelling (#11531)
1a81b52 
Hi, these are just some spelling corrections.

There is one I wasn't completely sure about in
src/Init/Data/List/Lemmas.lean:

> See also
> ...
> Also
> \* \`Init.Data.List.Monadic\` for **addiation** _(additional?)_ lemmas
about \`List.mapM\` and \`List.forM\`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

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

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

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

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

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

@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

@tom93 @nomeata @leanprover-community-bot @leanprover-bot