Extensional decidable equality for Std.HashMap?

Stream: lean4

[Siddharth Bhat]

I'd like to check if two Std.HashMaps are extensionally equal, in a Decidable fashion. Is there any API for this?

[Markus Himmel]

There are plans to provide a Std.ExtensionalHashMap which supports this, but the FRO is not planning to work on this soon.

[Eric Wieser]

Even without that, presumably we could have a BEq instance that evaluates extensional equality?

[Markus Himmel]

Yes, see here for example. The story is slightly more complicated for dependent hash maps which is why this wasn't part of the initial release of Std.HashMap, but we'll add it in the future.