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.

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

fix: naming convention for UInt lemmas #4514

Merged
merged 3 commits into from
Aug 12, 2024
Merged

fix: naming convention for UInt lemmas #4514

merged 3 commits into from
Aug 12, 2024

Conversation

fgdorais
Copy link
Contributor

Closes #4513

@fgdorais fgdorais requested a review from kim-em as a code owner June 20, 2024 13:04
@fgdorais fgdorais mentioned this pull request Jun 20, 2024
Open
@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 20, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Jun 20, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1f732bb3b7fa8e93ca01c1b257668aee14d72d2d --onto 357b52928f905bfb85a3496e411cf12fa20e730c. (2024-06-20 13:19:21)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1f732bb3b7fa8e93ca01c1b257668aee14d72d2d --onto 5426a5c8b36341fd1bf7a6088b519ae257a49fea. (2024-06-24 05:57:44)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4236d8a85b17fe1928613a1c300f89ace40a81f5 --onto 5f31e938c1bf5bb2d6d2d29b26ea932ade115357. (2024-08-12 01:05:42)

@kim-em
Copy link
Collaborator

kim-em commented Jun 24, 2024

@fgdorais could you please add @[deprecated (since := "2024-06-23")] abbrev foo := @bar for these? Happy to merge after that.

@kim-em kim-em self-assigned this Jun 24, 2024
@fgdorais
Copy link
Contributor Author

Deprecation completed. I kept these out of the theorem generating macro since I suppose they should eventually be removed. Let me know if you would rather have the deprecations inside the macro.

@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Aug 9, 2024
@kim-em kim-em enabled auto-merge August 12, 2024 00:42
@kim-em kim-em requested a review from TwoFX as a code owner August 12, 2024 00:49
@kim-em kim-em added this pull request to the merge queue Aug 12, 2024
Merged via the queue into leanprover:master with commit 759ece7 Aug 12, 2024
12 checks passed
Parcly-Taxel pushed a commit to Parcly-Taxel/lean4 that referenced this pull request Aug 12, 2024
@fgdorais @kim-em @Parcly-Taxel
fix: naming convention for UInt lemmas (leanprover#4514)
a554f90 
Closes leanprover#4513

---------

Co-authored-by: Kim Morrison <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

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

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

Assignees

@kim-em kim-em

Labels
P-medium We may work on this issue if we find the time 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.

Some uint lemmas do not follow correct naming conventions
5 participants
@fgdorais @leanprover-community-mathlib4-bot @kim-em @eric-wieser @leanprover-bot