BEq for HashMap / RBMap

Stream: lean4

[Eric Wieser]

Is it a deliverate choice not to implement these operators?

[Eric Wieser]

BEq (Std.HashMap _ _) and BEq (Lean.RBMap _ _ _) find no results on Loogle

[Paul Reichert]

I think we have these on our to-do list and just did not get around to implementing them yet. Agreed that we should have them eventually!

[Eric Wieser]

Are they not the same as equality on extensional hashmaps, and so easy to define with what already exists?

[Paul Reichert]

The equivalence relation (docs#Std.DHashMap.Raw.Equiv) on extensional hash maps is sensitive to the exact value of keys and values, not only their BEq equivalence class. I think this is necessary in order to define getKey and get; otherwise, what would they return? An element of a quotient type of keys or values?

Either way, I wouldn't say it would be difficult to implement a BEq instance (although we'd probably want a DecidableEq instance too, so there are also some proofs to be written). It's just not something we've come around so far.