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.empty_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{c : Nat}
:
Raw.empty c = (Raw₀.empty c).val
theorem
Std.DHashMap.Internal.Raw.emptyc_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
:
∅ = Raw₀.empty.val
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
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
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
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
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
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
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
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
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
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
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 ⋯
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
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
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
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
theorem
Std.DHashMap.Internal.Raw.filterMap_val
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
{m : Raw₀ α β}
{f : (a : α) → β a → Option (δ a)}
:
Raw.filterMap f m.val = (Raw₀.filterMap f m).val
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
theorem
Std.DHashMap.Internal.Raw.filter_val
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Raw₀ α β}
{f : (a : α) → β a → Bool}
:
Raw.filter f m.val = (Raw₀.filter f m).val
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
theorem
Std.DHashMap.Internal.Raw.Const.get?_val
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Raw₀ α fun (x : α) => β}
{a : α}
:
Raw.Const.get? m.val a = Raw₀.Const.get? m a
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 ⋯
theorem
Std.DHashMap.Internal.Raw.Const.get_val
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Raw₀ α fun (x : α) => β}
{a : α}
{h : a ∈ m.val}
:
Raw.Const.get m.val a h = Raw₀.Const.get m a ⋯
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
theorem
Std.DHashMap.Internal.Raw.Const.getD_val
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Raw₀ α fun (x : α) => β}
{a : α}
{fallback : β}
:
Raw.Const.getD m.val a fallback = Raw₀.Const.getD m a fallback
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
theorem
Std.DHashMap.Internal.Raw.Const.get!_val
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[Inhabited β]
{m : Raw₀ α fun (x : α) => β}
{a : α}
:
Raw.Const.get! m.val a = Raw₀.Const.get! m a
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
theorem
Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_snd_val
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Raw₀ α fun (x : α) => β}
{a : α}
{b : β}
:
(Raw.Const.getThenInsertIfNew? m.val a b).snd = (Raw₀.Const.getThenInsertIfNew? m a b).snd.val
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
theorem
Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_fst_val
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
{m : Raw₀ α fun (x : α) => β}
{a : α}
{b : β}
:
(Raw.Const.getThenInsertIfNew? m.val a b).fst = (Raw₀.Const.getThenInsertIfNew? m a b).fst