More lemmas about `Std.HashMap`

Stream: lean4

[Yuyang Zhao]

Are there any plans to add more lemmas about docs#Std.HashMap ? For example:

import Std.Data.HashMap

namespace Std.HashMap
variable {ι α : Type _} [BEq ι] [Hashable ι] [EquivBEq ι] [LawfulHashable ι] (c : HashMap ι α)

example : c.keys.Pairwise (fun a b => (a == b) = false) := sorry
example : i ∈ c.keys ↔ i ∈ c := sorry
example : c.keys.length = c.size := sorry

end Std.HashMap

[Markus Himmel]

Yes, verification of the keys function is on the FRO's TODO list. We're targeting early 2025 for this at the moment, but I cannot make any promises.

[Markus Himmel]

@Yuyang Zhao Good news: thanks to a contribution by @Lukas Gerlach and @Johannes Tantow these lemmas will be available in Lean v4.15.0 (to be released in December).