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

chore: rename HashMap.empty to HashMap.emptyWithCapacity #7447

Merged
merged 15 commits into from
Mar 12, 2025
Merged

chore: rename HashMap.empty to HashMap.emptyWithCapacity #7447

merged 15 commits into from
Mar 12, 2025

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Mar 12, 2025

This PR renames .empty with .emptyWithCapacity. This is a companion to #7445 for Array.

@kim-em kim-em requested a review from hargoniX as a code owner March 12, 2025 03:54
@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 12, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2952cf81e6089626f96321b44307d2222bc74d03 --onto 8fc8e8ed19ef218022f5a94cbf5e472e3b777e44. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-12 04:26:11)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 12, 2025 05:43 Inactive
TwoFX
TwoFX approved these changes Mar 12, 2025
View reviewed changes
Copy link
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.

I looked through the changes and everything looks good to me. Given that much of this PR was written by an AI, I'm not sure whether I should feel concerned or reassured...

@TwoFX TwoFX mentioned this pull request Mar 12, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Mar 12, 2025
@TwoFX
chore: rename insert_emptyc_eq to insert_empty_eq (#7451)
1a2345b 
This PR renames the member `insert_emptyc_eq` of the `LawfulSingleton`
typeclass to `insert_empty_eq` to conform to the recommended spelling of
`∅` as `empty`.

See also #7447.
@kim-em kim-em added this pull request to the merge queue Mar 12, 2025
Merged via the queue into master with commit a2cb435 Mar 12, 2025
15 checks passed
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

@mhuisi mhuisi Awaiting requested review from mhuisi mhuisi 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

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX 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.
3 participants
@kim-em @leanprover-community-bot @TwoFX