Skip to content
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.

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

chore: fix naming of several theorems #7499

Open
wants to merge 10 commits into
base: master
Choose a base branch
from

Conversation

Rob23oba
Copy link
Contributor

This PR fixes the spelling of several theorems to adhere to the naming convention.

Note: The changes here were found using a tool.

@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 15, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Mar 15, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a788e6aa6730ea901e17391c765d0b2508586bc5 --onto d5f01f2db1efd18034421ae2f40120d1c608f3c0. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-15 13:19:35)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5e0648fe988ccb6d25f369227daf21d78ce3030c --onto d32a7b250ad20477d55034488d89a050fbf70af5. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-17 18:08:23)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 53fcae031e5a37c7d8c0ac880f4da28929e3b932 --onto d32a7b250ad20477d55034488d89a050fbf70af5. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-18 17:02:45)
  • 💥 Mathlib branch lean-pr-testing-7499 build failed against this PR. (2025-03-19 16:33:25) View Log

@TwoFX TwoFX self-assigned this Mar 15, 2025
@TwoFX
Copy link
Member

TwoFX commented Mar 17, 2025

Thanks for doing this! I haven't gone through all files yet, but everything I've seen so far is looking great. I am assuming that the fallout in mathlib will be substantial, and there needs to be a mathlib branch ready for us to be able to merge this. At the same time this PR will accumulate marge conflicts quickly, so I suggest you try to rebase and get mathlib building quickly (and I'll be quick about merging once mathlib is building), possibly deferring the BitVec changes to a future PR to avoid merge conflicts here in core.

Update: I've gone through everything now, so I'm ready to hit merge once we have a mathlib build.

@Kha Kha added the awaiting-author Waiting for PR author to address issues label Mar 18, 2025
@Rob23oba Rob23oba force-pushed the naming-fixes branch 3 times, most recently from 91aaa32 to 7c9a084 Compare March 19, 2025 14:08
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 19, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 19, 2025
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 19, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-author Waiting for PR author to address issues breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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