Lemmas for Batteries.HashMap

Note that Lean core provides an alternative hash map implementation, Std.HashMap, which comes with more lemmas. See the module Std.Data.HashMap.Lemmas.

@[simp]

theorem Batteries.HashMap.Imp.empty_buckets {α : Type u_1} {β : Type u_2} : Batteries.HashMap.Imp.empty.buckets = ⟨mkArray 8 Batteries.AssocList.nil, ⋯⟩

@[simp]

theorem Batteries.HashMap.Imp.empty_val {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : ∅.val = Batteries.HashMap.Imp.empty

@[simp]

theorem Batteries.HashMap.empty_find? {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {a : α} : ∅.find? a = none