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}
:
Std.DHashMap.Internal.List.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), (Std.DHashMap.Internal.mkIdx size h' (hash k)).val.toNat = i)
:
Std.DHashMap.Internal.List.HashesTo l i size → Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.HashesTo l i size)
(k : α)
:
(Std.DHashMap.Internal.mkIdx size hs (hash k)).val.toNat ≠ i → Std.DHashMap.Internal.List.containsKey k l = false