Closed kim-em closed 5 days ago
This PR adds deprecations for Lean.HashMap functions which did not receive deprecation attributes initially.
Lean.HashMap
(Requested on zulip.)
Note that I've used the original deprecation date of 2024-08-08, when the type itself was deprecated; this will not delay removal.
Mathlib CI status (docs):
nightly-with-mathlib
git rebase bf13b24692ce5b96cb8a9fd4a3d11c0e170dbccf --onto ba3f2b3ecf8967410f3498e2835b883601f03967
This PR adds deprecations for
Lean.HashMap
functions which did not receive deprecation attributes initially.(Requested on zulip.)
Note that I've used the original deprecation date of 2024-08-08, when the type itself was deprecated; this will not delay removal.