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

feat: (DHashMap|HashMap|HashSet).(getKey?|getKey|getKey!|getKeyD) #5244

Merged
merged 18 commits into from
Sep 13, 2024
Merged

feat: (DHashMap|HashMap|HashSet).(getKey?|getKey|getKey!|getKeyD) #5244

merged 18 commits into from
Sep 13, 2024

Conversation

hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Sep 3, 2024

No description provided.

@hargoniX hargoniX requested a review from TwoFX as a code owner September 3, 2024 14:05
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc September 3, 2024 14:17 Inactive
@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 Sep 3, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 3, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5244
bb3bc63
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 3, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5244
e77557d
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Sep 3, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@hargoniX hargoniX added the awaiting-review Waiting for someone to review the PR label Sep 3, 2024
TwoFX
TwoFX reviewed Sep 4, 2024
View reviewed changes
src/Std/Data/HashSet/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/HashSet/Basic.lean Outdated Show resolved Hide resolved
src/Std/Data/HashSet/Basic.lean Outdated Show resolved Hide resolved
@TwoFX TwoFX added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Sep 5, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc September 6, 2024 10:18 Inactive
@leanprover-community-mathlib4-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 eba0cbaeb0f70473aed05541b7ba066ad8492e23 --onto 1b099521c1bfd5fbcbb90808396b767f0bb3e661. (2024-09-06 10:28:07)

@hargoniX hargoniX requested a review from TwoFX September 6, 2024 11:09
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc September 6, 2024 11:18 Inactive
@hargoniX hargoniX added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Sep 9, 2024
@TwoFX TwoFX added this pull request to the merge queue Sep 13, 2024
Merged via the queue into master with commit 2080fc0 Sep 13, 2024
17 checks passed
tobiasgrosser pushed a commit to opencompl/lean4 that referenced this pull request Sep 16, 2024
@hargoniX @tobiasgrosser
feat: (DHashMap|HashMap|HashSet).(getKey?|getKey|getKey!|…
8c9644f 
…`getKeyD`) (leanprover#5244)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

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

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR 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
@hargoniX @leanprover-community-bot @leanprover-community-mathlib4-bot @TwoFX