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₀
theorem
Std.DHashMap.Internal.Raw.insert_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
{b : β a}
:
m.insert a b = (Std.DHashMap.Internal.Raw₀.insert ⟨m, ⋯⟩ a b).val
theorem
Std.DHashMap.Internal.Raw.insert_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
{b : β a}
:
m.val.insert a b = (m.insert a b).val
theorem
Std.DHashMap.Internal.Raw.insertIfNew_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
{b : β a}
:
m.insertIfNew a b = (Std.DHashMap.Internal.Raw₀.insertIfNew ⟨m, ⋯⟩ a b).val
theorem
Std.DHashMap.Internal.Raw.insertIfNew_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
{b : β a}
:
m.val.insertIfNew a b = (m.insertIfNew a b).val
theorem
Std.DHashMap.Internal.Raw.containsThenInsert_snd_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
{b : β a}
:
(m.containsThenInsert a b).snd = (Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨m, ⋯⟩ a b).snd.val
theorem
Std.DHashMap.Internal.Raw.containsThenInsert_snd_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
{b : β a}
:
(m.val.containsThenInsert a b).snd = (m.containsThenInsert a b).snd.val
theorem
Std.DHashMap.Internal.Raw.containsThenInsert_fst_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
{b : β a}
:
(m.containsThenInsert a b).fst = (Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨m, ⋯⟩ a b).fst
theorem
Std.DHashMap.Internal.Raw.containsThenInsert_fst_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
{b : β a}
:
(m.val.containsThenInsert a b).fst = (m.containsThenInsert a b).fst
theorem
Std.DHashMap.Internal.Raw.containsThenInsertIfNew_snd_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
{b : β a}
:
(m.containsThenInsertIfNew a b).snd = (Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew ⟨m, ⋯⟩ a b).snd.val
theorem
Std.DHashMap.Internal.Raw.containsThenInsertIfNew_snd_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
{b : β a}
:
(m.val.containsThenInsertIfNew a b).snd = (m.containsThenInsertIfNew a b).snd.val
theorem
Std.DHashMap.Internal.Raw.containsThenInsertIfNew_fst_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
{b : β a}
:
(m.containsThenInsertIfNew a b).fst = (Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew ⟨m, ⋯⟩ a b).fst
theorem
Std.DHashMap.Internal.Raw.containsThenInsertIfNew_fst_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
{b : β a}
:
(m.val.containsThenInsertIfNew a b).fst = (m.containsThenInsertIfNew a b).fst
theorem
Std.DHashMap.Internal.Raw.getThenInsertIfNew?_snd_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
{b : β a}
:
(m.getThenInsertIfNew? a b).snd = (Std.DHashMap.Internal.Raw₀.getThenInsertIfNew? ⟨m, ⋯⟩ a b).snd.val
theorem
Std.DHashMap.Internal.Raw.getThenInsertIfNew?_snd_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
{b : β a}
:
(m.val.getThenInsertIfNew? a b).snd = (m.getThenInsertIfNew? a b).snd.val
theorem
Std.DHashMap.Internal.Raw.getThenInsertIfNew?_fst_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
{b : β a}
:
(m.getThenInsertIfNew? a b).fst = (Std.DHashMap.Internal.Raw₀.getThenInsertIfNew? ⟨m, ⋯⟩ a b).fst
theorem
Std.DHashMap.Internal.Raw.getThenInsertIfNew?_fst_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
{b : β a}
:
(m.val.getThenInsertIfNew? a b).fst = (m.getThenInsertIfNew? a b).fst
theorem
Std.DHashMap.Internal.Raw.get?_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
:
m.get? a = Std.DHashMap.Internal.Raw₀.get? ⟨m, ⋯⟩ a
theorem
Std.DHashMap.Internal.Raw.get?_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
:
m.val.get? a = m.get? a
theorem
Std.DHashMap.Internal.Raw.contains_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
:
m.contains a = Std.DHashMap.Internal.Raw₀.contains ⟨m, ⋯⟩ a
theorem
Std.DHashMap.Internal.Raw.contains_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
:
m.val.contains a = m.contains a
theorem
Std.DHashMap.Internal.Raw.get_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Raw α β}
{a : α}
{h : a ∈ m}
:
m.get a h = Std.DHashMap.Internal.Raw₀.get ⟨m, ⋯⟩ a ⋯
theorem
Std.DHashMap.Internal.Raw.get_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
{h : a ∈ m.val}
:
m.val.get a h = m.get a ⋯
theorem
Std.DHashMap.Internal.Raw.getD_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
{fallback : β a}
:
m.getD a fallback = Std.DHashMap.Internal.Raw₀.getD ⟨m, ⋯⟩ a fallback
theorem
Std.DHashMap.Internal.Raw.getD_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
{fallback : β a}
:
m.val.getD a fallback = m.getD a fallback
theorem
Std.DHashMap.Internal.Raw.get!_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
[Inhabited (β a)]
:
m.get! a = Std.DHashMap.Internal.Raw₀.get! ⟨m, ⋯⟩ a
theorem
Std.DHashMap.Internal.Raw.get!_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
[Inhabited (β a)]
:
m.val.get! a = m.get! a
theorem
Std.DHashMap.Internal.Raw.erase_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{a : α}
:
m.erase a = (Std.DHashMap.Internal.Raw₀.erase ⟨m, ⋯⟩ a).val
theorem
Std.DHashMap.Internal.Raw.erase_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
:
m.val.erase a = (m.erase a).val
theorem
Std.DHashMap.Internal.Raw.filterMap_eq
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{f : (a : α) → β a → Option (δ a)}
:
Std.DHashMap.Raw.filterMap f m = (Std.DHashMap.Internal.Raw₀.filterMap f ⟨m, ⋯⟩).val
theorem
Std.DHashMap.Internal.Raw.filterMap_val
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → Option (δ a)}
:
Std.DHashMap.Raw.filterMap f m.val = (Std.DHashMap.Internal.Raw₀.filterMap f m).val
theorem
Std.DHashMap.Internal.Raw.map_eq
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{f : (a : α) → β a → δ a}
:
Std.DHashMap.Raw.map f m = (Std.DHashMap.Internal.Raw₀.map f ⟨m, ⋯⟩).val
theorem
Std.DHashMap.Internal.Raw.map_val
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → δ a}
:
Std.DHashMap.Raw.map f m.val = (Std.DHashMap.Internal.Raw₀.map f m).val
theorem
Std.DHashMap.Internal.Raw.filter_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
{f : (a : α) → β a → Bool}
:
Std.DHashMap.Raw.filter f m = (Std.DHashMap.Internal.Raw₀.filter f ⟨m, ⋯⟩).val
theorem
Std.DHashMap.Internal.Raw.filter_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → Bool}
:
Std.DHashMap.Raw.filter f m.val = (Std.DHashMap.Internal.Raw₀.filter f m).val
theorem
Std.DHashMap.Internal.Raw.Const.get?_eq
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α fun (x : α) => β}
(h : m.WF)
{a : α}
:
theorem
Std.DHashMap.Internal.Raw.Const.get?_val
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
{a : α}
:
theorem
Std.DHashMap.Internal.Raw.Const.get_eq
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α fun (x : α) => β}
{a : α}
{h : a ∈ m}
:
Std.DHashMap.Raw.Const.get m a h = Std.DHashMap.Internal.Raw₀.Const.get ⟨m, ⋯⟩ a ⋯
theorem
Std.DHashMap.Internal.Raw.Const.get_val
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
{a : α}
{h : a ∈ m.val}
:
Std.DHashMap.Raw.Const.get m.val a h = Std.DHashMap.Internal.Raw₀.Const.get m a ⋯
theorem
Std.DHashMap.Internal.Raw.Const.getD_eq
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α fun (x : α) => β}
(h : m.WF)
{a : α}
{fallback : β}
:
Std.DHashMap.Raw.Const.getD m a fallback = Std.DHashMap.Internal.Raw₀.Const.getD ⟨m, ⋯⟩ a fallback
theorem
Std.DHashMap.Internal.Raw.Const.getD_val
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
{a : α}
{fallback : β}
:
Std.DHashMap.Raw.Const.getD m.val a fallback = Std.DHashMap.Internal.Raw₀.Const.getD m a fallback
theorem
Std.DHashMap.Internal.Raw.Const.get!_eq
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[Inhabited β]
{m : Std.DHashMap.Raw α fun (x : α) => β}
(h : m.WF)
{a : α}
:
theorem
Std.DHashMap.Internal.Raw.Const.get!_val
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[Inhabited β]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
{a : α}
:
theorem
Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_snd_eq
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α fun (x : α) => β}
(h : m.WF)
{a : α}
{b : β}
:
(Std.DHashMap.Raw.Const.getThenInsertIfNew? m a b).snd = (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? ⟨m, ⋯⟩ a b).snd.val
theorem
Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_snd_val
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
{a : α}
{b : β}
:
(Std.DHashMap.Raw.Const.getThenInsertIfNew? m.val a b).snd = (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m a b).snd.val
theorem
Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_fst_eq
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α fun (x : α) => β}
(h : m.WF)
{a : α}
{b : β}
:
(Std.DHashMap.Raw.Const.getThenInsertIfNew? m a b).fst = (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? ⟨m, ⋯⟩ a b).fst
theorem
Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_fst_val
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
{a : α}
{b : β}
:
(Std.DHashMap.Raw.Const.getThenInsertIfNew? m.val a b).fst = (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m a b).fst