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: relating operations on `Raw` to operations on `Raw₀`

source
theorem Std.DHashMap.Internal.Raw.empty_eq {α : Type u} {β : α → Type v} {c : Nat} :
Raw.emptyWithCapacity c = (Raw₀.emptyWithCapacity c).val
source
theorem Std.DHashMap.Internal.Raw.emptyc_eq {α : Type u} {β : α → Type v} :
∅ = Raw₀.emptyWithCapacity.val
source
theorem Std.DHashMap.Internal.Raw.insert_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
m.insert a b = (Raw₀.insert ⟨m, ⋯⟩ a b).val
source
theorem Std.DHashMap.Internal.Raw.insertIfNew_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
m.insertIfNew a b = (Raw₀.insertIfNew ⟨m, ⋯⟩ a b).val
source
theorem Std.DHashMap.Internal.Raw.containsThenInsert_snd_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
(m.containsThenInsert a b).snd = (Raw₀.containsThenInsert ⟨m, ⋯⟩ a b).snd.val
source
theorem Std.DHashMap.Internal.Raw.containsThenInsert_fst_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
(m.containsThenInsert a b).fst = (Raw₀.containsThenInsert ⟨m, ⋯⟩ a b).fst
source
theorem Std.DHashMap.Internal.Raw.containsThenInsertIfNew_snd_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
(m.containsThenInsertIfNew a b).snd = (Raw₀.containsThenInsertIfNew ⟨m, ⋯⟩ a b).snd.val
source
theorem Std.DHashMap.Internal.Raw.containsThenInsertIfNew_fst_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
(m.containsThenInsertIfNew a b).fst = (Raw₀.containsThenInsertIfNew ⟨m, ⋯⟩ a b).fst
source
theorem Std.DHashMap.Internal.Raw.getThenInsertIfNew?_snd_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
(m.getThenInsertIfNew? a b).snd = (Raw₀.getThenInsertIfNew? ⟨m, ⋯⟩ a b).snd.val
source
theorem Std.DHashMap.Internal.Raw.getThenInsertIfNew?_fst_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
(m.getThenInsertIfNew? a b).fst = (Raw₀.getThenInsertIfNew? ⟨m, ⋯⟩ a b).fst
source
theorem Std.DHashMap.Internal.Raw.get?_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α} :
m.get? a = Raw₀.get? ⟨m, ⋯⟩ a
source
theorem Std.DHashMap.Internal.Raw.contains_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} :
m.contains a = Raw₀.contains ⟨m, ⋯⟩ a
source
theorem Std.DHashMap.Internal.Raw.get_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {a : α} {h : a ∈ m} :
m.get a h = Raw₀.get ⟨m, ⋯⟩ a ⋯
source
theorem Std.DHashMap.Internal.Raw.getD_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α} {fallback : β a} :
m.getD a fallback = Raw₀.getD ⟨m, ⋯⟩ a fallback
source
theorem Std.DHashMap.Internal.Raw.get!_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α} [Inhabited (β a)] :
m.get! a = Raw₀.get! ⟨m, ⋯⟩ a
source
theorem Std.DHashMap.Internal.Raw.getKey?_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} :
m.getKey? a = Raw₀.getKey? ⟨m, ⋯⟩ a
source
theorem Std.DHashMap.Internal.Raw.getKey_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} {a : α} {h : a ∈ m} :
m.getKey a h = Raw₀.getKey ⟨m, ⋯⟩ a ⋯
source
theorem Std.DHashMap.Internal.Raw.getKeyD_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a fallback : α} :
m.getKeyD a fallback = Raw₀.getKeyD ⟨m, ⋯⟩ a fallback
source
theorem Std.DHashMap.Internal.Raw.getKey!_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [Inhabited α] {m : Raw α β} (h : m.WF) {a : α} :
m.getKey! a = Raw₀.getKey! ⟨m, ⋯⟩ a
source
theorem Std.DHashMap.Internal.Raw.erase_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} :
m.erase a = (Raw₀.erase ⟨m, ⋯⟩ a).val
source
theorem Std.DHashMap.Internal.Raw.filterMap_eq {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) → β a → Option (δ a)} :
Raw.filterMap f m = (Raw₀.filterMap f ⟨m, ⋯⟩).val
source
theorem Std.DHashMap.Internal.Raw.map_eq {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) → β a → δ a} :
Raw.map f m = (Raw₀.map f ⟨m, ⋯⟩).val
source
theorem Std.DHashMap.Internal.Raw.filter_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) → β a → Bool} :
Raw.filter f m = (Raw₀.filter f ⟨m, ⋯⟩).val
source
theorem Std.DHashMap.Internal.Raw.insertMany_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {l : ρ} :
m.insertMany l = (Raw₀.insertMany ⟨m, ⋯⟩ l).val.val
source
theorem Std.DHashMap.Internal.Raw.ofList_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {l : List ((a : α) × β a)} :
Raw.ofList l = (Raw₀.emptyWithCapacity.insertMany l).val.val
source
theorem Std.DHashMap.Internal.Raw.alter_eq {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] {m : Raw α β} (h : m.WF) {k : α} {f : Option (β k) → Option (β k)} :
m.alter k f = (Raw₀.alter ⟨m, ⋯⟩ k f).val
source
theorem Std.DHashMap.Internal.Raw.modify_eq {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] {m : Raw α β} (h : m.WF) {k : α} {f : β k → β k} :
m.modify k f = (Raw₀.modify ⟨m, ⋯⟩ k f).val
source
theorem Std.DHashMap.Internal.Raw.union_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) :
m₁.union m₂ = (Raw₀.union ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩).val
source
theorem Std.DHashMap.Internal.Raw.Const.insertMany_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {ρ : Type w} [ForIn Id ρ (α × β)] {l : ρ} :
Raw.Const.insertMany m l = (Raw₀.Const.insertMany ⟨m, ⋯⟩ l).val.val
source
theorem Std.DHashMap.Internal.Raw.Const.ofList_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {l : List (α × β)} :
Raw.Const.ofList l = (Raw₀.Const.insertMany Raw₀.emptyWithCapacity l).val.val
source
theorem Std.DHashMap.Internal.Raw.Const.insertManyIfNewUnit_eq {α : Type u} {ρ : Type w} [ForIn Id ρ α] [BEq α] [Hashable α] {m : Raw α fun (x : α) => Unit} {l : ρ} (h : m.WF) :
Raw.Const.insertManyIfNewUnit m l = (Raw₀.Const.insertManyIfNewUnit ⟨m, ⋯⟩ l).val.val
source
theorem Std.DHashMap.Internal.Raw.Const.unitOfList_eq {α : Type u} [BEq α] [Hashable α] {l : List α} :
Raw.Const.unitOfList l = (Raw₀.Const.insertManyIfNewUnit Raw₀.emptyWithCapacity l).val.val
source
theorem Std.DHashMap.Internal.Raw.Const.get?_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {a : α} :
Raw.Const.get? m a = Raw₀.Const.get? ⟨m, ⋯⟩ a
source
theorem Std.DHashMap.Internal.Raw.Const.get_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw α fun (x : α) => β} {a : α} {h : a ∈ m} :
Raw.Const.get m a h = Raw₀.Const.get ⟨m, ⋯⟩ a ⋯
source
theorem Std.DHashMap.Internal.Raw.Const.getD_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {a : α} {fallback : β} :
Raw.Const.getD m a fallback = Raw₀.Const.getD ⟨m, ⋯⟩ a fallback
source
theorem Std.DHashMap.Internal.Raw.Const.get!_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] {m : Raw α fun (x : α) => β} (h : m.WF) {a : α} :
Raw.Const.get! m a = Raw₀.Const.get! ⟨m, ⋯⟩ a
source
theorem Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_snd_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {a : α} {b : β} :
(Raw.Const.getThenInsertIfNew? m a b).snd = (Raw₀.Const.getThenInsertIfNew? ⟨m, ⋯⟩ a b).snd.val
source
theorem Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_fst_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {a : α} {b : β} :
(Raw.Const.getThenInsertIfNew? m a b).fst = (Raw₀.Const.getThenInsertIfNew? ⟨m, ⋯⟩ a b).fst
source
theorem Std.DHashMap.Internal.Raw.Const.alter_eq {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {k : α} {f : Option β → Option β} :
Raw.Const.alter m k f = (Raw₀.Const.alter ⟨m, ⋯⟩ k f).val
source
theorem Std.DHashMap.Internal.Raw.Const.modify_eq {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {k : α} {f : β → β} :
Raw.Const.modify m k f = (Raw₀.Const.modify ⟨m, ⋯⟩ k f).val