Skip to content

fix: rename Int.sq_nonnneg to Int.sq_nonneg#12909

Merged
TwoFX merged 2 commits intoleanprover:masterfrom
b-mehta:fix-sq-nonneg-typo
Mar 16, 2026
Merged

fix: rename Int.sq_nonnneg to Int.sq_nonneg#12909
TwoFX merged 2 commits intoleanprover:masterfrom
b-mehta:fix-sq-nonneg-typo

Conversation

@b-mehta
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta commented Mar 13, 2026

This PR fixes the typo in Int.sq_nonnneg.

Closes #12906.

@b-mehta @claude
fix: rename Int.sq_nonnneg to Int.sq_nonneg
0154681 
Closes leanprover#12906

Co-authored-by: Claude <noreply@anthropic.com>
@b-mehta b-mehta requested a review from kim-em as a code owner March 13, 2026 16:43
@b-mehta
Copy link
Copy Markdown
Contributor Author

b-mehta commented Mar 13, 2026

changelog-library

@github-actions github-actions bot added the changelog-library Library label Mar 13, 2026
@b-mehta @claude
fix: qualify deprecated alias name
3579fa3 
Co-authored-by: Claude <noreply@anthropic.com>
@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 Mar 13, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 13, 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 de2b177423aeceb5ae9c1db331509d39df3b6720 --onto e8048291010c815d0d30926924e7ad7afc18b1c0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-13 17:54:49)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 13, 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 de2b177423aeceb5ae9c1db331509d39df3b6720 --onto e6d9220eee278116b0bd28f9ec19388fdc690180. You can force reference manual CI using the force-manual-ci label. (2026-03-13 17:54:51)

TwoFX
TwoFX approved these changes Mar 16, 2026
View reviewed changes
Copy link
Copy Markdown
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@TwoFX TwoFX added this pull request to the merge queue Mar 16, 2026
Merged via the queue into leanprover:master with commit 76e593a Mar 16, 2026
17 checks passed
@b-mehta b-mehta deleted the fix-sq-nonneg-typo branch March 17, 2026 15:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX TwoFX approved these changes

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

Assignees

No one assigned

Labels

changelog-library Library 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.

typo in declaration Int.sq_nonnneg

3 participants

@b-mehta @leanprover-bot @TwoFX