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.

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

feat: lemmas for HashMap.alter and .modify #6620

Merged
merged 42 commits into from
Jan 21, 2025
Merged

feat: lemmas for HashMap.alter and .modify #6620

merged 42 commits into from
Jan 21, 2025

Conversation

datokrat
Copy link
Contributor

@datokrat datokrat commented Jan 13, 2025

This PR adds lemmas about HashMap.alter and .modify. These lemmas describe the interaction of alter and modify with the read methods of the HashMap. The additions affect the HashMap, the DHashMap and their respective raw versions. Moreover, the raw versions of alter and modify are defined.

@datokrat datokrat added the WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet. label Jan 13, 2025
@datokrat datokrat changed the base branch from master to paul/alter-alter January 13, 2025 09:18
@datokrat datokrat changed the base branch from paul/alter-alter to master January 13, 2025 09:18
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Lemmas.lean Show resolved Hide resolved
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
@datokrat datokrat changed the base branch from master to paul/alter-alter January 13, 2025 14:54
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 16, 2025 10:20 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 Jan 16, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 16, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 16, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 16, 2025

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-6620 has successfully built against this PR. (2025-01-16 11:04:50) View Log
  • ✅ Mathlib branch lean-pr-testing-6620 has successfully built against this PR. (2025-01-17 15:25:22) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1d03cd6a6b9e2cab387692f5ec0d0013b9a9867d --onto 74bd40d34d1a969da65007939960c2fefd461f08. (2025-01-20 12:17:49)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1d03cd6a6b9e2cab387692f5ec0d0013b9a9867d --onto ac6a29ee834ba7fd30e9372e51493d7741e9c657. (2025-01-21 10:36:21)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 35697973771b8dbbbb6b3872a40cc604764d36ae --onto f9e904af5022a57adb6105cda65d1569449346c2. (2025-01-21 12:36:39)

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jan 16, 2025
@datokrat
Copy link
Contributor Author

datokrat commented Jan 16, 2025

@TwoFX The DHashMap lemmas are done now. Note that there are still some out-commented lemmas in case I happen to need them when I proceed. Next I'll do Raw and HashMap. (Keeping the MyRawLemmas file for now to speed up compilation during development)

@datokrat datokrat marked this pull request as ready for review January 17, 2025 14:16
@datokrat datokrat removed the WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet. label Jan 17, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 17, 2025 14:31 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 17, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 17, 2025
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/HashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/HashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/HashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/HashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/HashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/HashMap/Lemmas.lean Outdated Show resolved Hide resolved
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 20, 2025 11:49 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 20, 2025 12:03 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 20, 2025 13:19 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 20, 2025 13:50 Inactive
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Lemmas.lean Outdated Show resolved Hide resolved
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 21, 2025 10:12 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 21, 2025 10:26 Inactive
@TwoFX TwoFX enabled auto-merge January 21, 2025 12:21
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 21, 2025 12:24 Inactive
@TwoFX TwoFX added this pull request to the merge queue Jan 21, 2025
Merged via the queue into master with commit 31929c0 Jan 21, 2025
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants