Skip to content

chore: deprecate Lean.HashMap and Lean.HashSet#4954

Merged
TwoFX merged 2 commits intomasterfrom
deprecate-hashmap
Aug 8, 2024
Merged

chore: deprecate Lean.HashMap and Lean.HashSet#4954
TwoFX merged 2 commits intomasterfrom
deprecate-hashmap

Conversation

@TwoFX
Copy link
Member

@TwoFX TwoFX commented Aug 8, 2024

This restores all of the imports of Lean.Data.HashMap and Lean.Data.HashSet so that users actually see the deprecation warnings instead of a "declaration not found" error.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 8, 2024 09:46 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 Aug 8, 2024
@ghost
Copy link

ghost commented Aug 8, 2024

Mathlib CI status (docs):

  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-08-08 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-08-08 09:58:06)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-08-08 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-08-08 12:46:55)

@TwoFX TwoFX requested review from leodemoura and tydeu as code owners August 8, 2024 12:31
@TwoFX TwoFX enabled auto-merge August 8, 2024 12:33
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 8, 2024 12:40 Inactive
@TwoFX TwoFX added this pull request to the merge queue Aug 8, 2024
Merged via the queue into master with commit b144107 Aug 8, 2024
@TwoFX TwoFX deleted the deprecate-hashmap branch August 4, 2025 07:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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.

1 participant