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: equivalence on hash maps #7341

Draft
wants to merge 5 commits into
base: master
Choose a base branch
from
Draft

feat: equivalence on hash maps #7341

wants to merge 5 commits into from

Conversation

Rob23oba
Copy link
Contributor

@Rob23oba Rob23oba commented Mar 5, 2025

This PR adds an equivalence relation to the hash map with several lemmas for it.

@Rob23oba Rob23oba changed the title feat: equivalence on DHashMap.Raw and simple lemmas feat: equivalence on hash maps Mar 5, 2025
@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 5, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Mar 5, 2025 •
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 64731b71aad34943937283d39930b12db4bb16da --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-05 08:45:46)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 68f3fc6d5d58bfacf50031a6662b64b399988dee --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-05 19:07:42)

@TwoFX TwoFX self-assigned this Mar 5, 2025
TwoFX
TwoFX reviewed Mar 5, 2025
View reviewed changes
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX TwoFX left review comments

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

Assignees

@TwoFX TwoFX

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
@Rob23oba @leanprover-community-bot @TwoFX