Std.HashSet.merge missing

Stream: lean4

[Adam Topaz]

I was using Lean.HashSet.merge in one of my projects, and after updating today, I got a deprecation warning that Lean.HashSet has been deprecated and that I should use Std.HashSet instead. However, it seems that functions like docs#Lean.HashSet.merge have not been moved over. Is this intentional?

[Henrik Böving]

CC @Markus Himmel

[Markus Himmel]

You should be able to use docs#Std.HashSet.insertMany

[Adam Topaz]

Well, I ended up just using a fold, so it's not a big deal for my purposes. I was just wondering if this was an oversight.

[Adam Topaz]

in principle one could also introduce an instance of docs#Union

[Kim Morrison]

There's also HashSet.union.