operations on HashMap

Stream: std4

[Scott Morrison]

I'll need some additional operations on HashMap soon, in particular map (applying a function to each value), and constructing the pointwise addition of two HashMaps (valued in an AddMonoid).

Neither of these exist at present, as far as I can see. If anyone has plans to do either of them, please let me know. :-)

I assume map should go in Std4, while the pointwise operations should go in mathlib4 (simply because the algebraic typeclasses are there for now).

[Mario Carneiro]

I'm working on hashmaps now, I can add map

[Scott Morrison]

Maybe it should be called mapVal for consistency for AssocList.

[Mario Carneiro]

ok, mapVal and mergeWith are now in std

[Mario Carneiro]

you should pass + as the combining function for your AddMonoid use case

[Scott Morrison]

Great, thanks!

[Scott Morrison]

I'd also like filter (filtering keys) on HashMap. Do you want to also add that in std?

After that I'll need a HashSet with .union and .sdiff. I can just do a minimal version of those for now, defining HashSet k := HashMap k Unit somewhere.