This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file.

File contents: lemmas about HashesTo (defined in Internal.Defs)

@[simp]

theorem Std.DHashMap.Internal.List.hashesTo_nil {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {i size : Nat} : HashesTo [] i size

theorem Std.DHashMap.Internal.List.hashesTo_cons {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {i size : Nat} {l : List ((a : α) × β a)} {k : α} {v : β k} (h : ∀ (h' : 0 < size), (mkIdx size h' (hash k)).val.toNat = i) : HashesTo l i size → HashesTo (⟨k, v⟩ :: l) i size

theorem Std.DHashMap.Internal.List.HashesTo.containsKey_eq_false {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulHashable α] {l : List ((a : α) × β a)} {i size : Nat} (hs : 0 < size) (h : HashesTo l i size) (k : α) : (mkIdx size hs (hash k)).val.toNat ≠ i → containsKey k l = false