Skip to content

feat: add union on ExtDTHashMap/ExtHashMap/ExtHashSet #10946

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
Draft
wants to merge 13 commits into
base: master
Choose a base branch
from
Draft

feat: add union on ExtDTHashMap/ExtHashMap/ExtHashSet #10946

wants to merge 13 commits into from
+714 −3

Conversation

@wkrozowski
Copy link
Contributor

This PR adds union operation on ExtDHashMap/ExtHashMap/ExtHashSet nd provides lemmas about union operations.

@wkrozowski wkrozowski marked this pull request as draft October 27, 2025 12:45
@wkrozowski wkrozowski force-pushed the wojciech/extdhashmap_union2 branch from 1cf8380 to 7887726 Compare October 27, 2025 12:45
@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 Oct 27, 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 12750d25b5651a87f3ec89d7ec2669c711cbac4f --onto 97d63db52cd2fc3353f8a75f48209de0011f1bd3. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-27 13:45:58)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 12750d25b5651a87f3ec89d7ec2669c711cbac4f --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-27 13:46:00)

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

changelog-library Library 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

@wkrozowski @leanprover-community-bot @leanprover-bot