Transition to `Std.HashMap`

Stream: lean4

[Patrick Massot]

I’m trying to bump the Lean version of Verbose Lean from 4.10.0 to 4.15.0-rc1 and I gets tons of deprecation warnings because I use Lean.HashMap. I’m willing to switch to Std.HashMap but I don’t want to give up my open Lean. What is the preferred solution?

[Yaël Dillies]

Does open Lean hiding HashMap work for you?

[Yaël Dillies]

(maybe the new API doesn't conflict in name with the old one, meaning you don't have to do open Lean hiding HashMap HashMap.lemma_1 HashMap.lemma_2 ...)

[Patrick Massot]

I was worried about that second message, but it doesn’t seem too bad in my case anyway.