Skip to content

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

Merged
TwoFX merged 18 commits into
masterfrom
hashmap-getKey
Sep 13, 2024
Merged

feat: (DHashMap|HashMap|HashSet).(getKey?|getKey|getKey!|getKeyD)#5244
TwoFX merged 18 commits into
masterfrom
hashmap-getKey

Conversation

@hargoniX

@hargoniX hargoniX commented Sep 3, 2024

Copy link
Copy Markdown
Member

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
ghost pushed 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
ghost pushed 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
@ghost ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Sep 3, 2024
@ghost

ghost commented Sep 3, 2024

Copy link
Copy Markdown

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
Comment thread src/Std/Data/HashSet/Lemmas.lean Outdated
Comment thread src/Std/Data/HashSet/Basic.lean Outdated
Comment thread src/Std/Data/HashSet/Basic.lean Outdated
@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
@ghost

ghost commented Sep 6, 2024

Copy link
Copy Markdown

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
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.

2 participants

@hargoniX @TwoFX