Documentation

Std.Data.DHashMap.Internal.Raw

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.emptyc_eq {α : Type u} {β : αType v} [BEq α] [Hashable α] :
= Std.DHashMap.Internal.Raw₀.empty.val
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.getKey?_eq {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α} :
m.getKey? a = Std.DHashMap.Internal.Raw₀.getKey? m, a
theorem Std.DHashMap.Internal.Raw.getKey?_val {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Internal.Raw₀ α β} {a : α} :
m.val.getKey? a = m.getKey? a
theorem Std.DHashMap.Internal.Raw.getKey_eq {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} {a : α} {h : a m} :
m.getKey a h = Std.DHashMap.Internal.Raw₀.getKey m, a
theorem Std.DHashMap.Internal.Raw.getKey_val {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Internal.Raw₀ α β} {a : α} {h : a m.val} :
m.val.getKey a h = m.getKey a
theorem Std.DHashMap.Internal.Raw.getKeyD_eq {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α} {fallback : α} :
m.getKeyD a fallback = Std.DHashMap.Internal.Raw₀.getKeyD m, a fallback
theorem Std.DHashMap.Internal.Raw.getKeyD_val {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Internal.Raw₀ α β} {a : α} {fallback : α} :
m.val.getKeyD a fallback = m.getKeyD a fallback
theorem Std.DHashMap.Internal.Raw.getKey!_eq {α : Type u} {β : αType v} [BEq α] [Hashable α] [Inhabited α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α} :
m.getKey! a = Std.DHashMap.Internal.Raw₀.getKey! m, a
theorem Std.DHashMap.Internal.Raw.getKey!_val {α : Type u} {β : αType v} [BEq α] [Hashable α] [Inhabited α] {m : Std.DHashMap.Internal.Raw₀ α β} {a : α} :
m.val.getKey! a = m.getKey! 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 : α) → β aOption (δ a)} :
theorem Std.DHashMap.Internal.Raw.filterMap_val {α : Type u} {β : αType v} {δ : αType w} [BEq α] [Hashable α] {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β aOption (δ a)} :
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} :
theorem Std.DHashMap.Internal.Raw.map_val {α : Type u} {β : αType v} {δ : αType w} [BEq α] [Hashable α] {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β aδ a} :
theorem Std.DHashMap.Internal.Raw.filter_eq {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {f : (a : α) → β aBool} :
theorem Std.DHashMap.Internal.Raw.filter_val {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β aBool} :
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_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α fun (x : α) => β} {a : α} {h : a m} :
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} :
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 : β} :
theorem Std.DHashMap.Internal.Raw.Const.getD_val {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β} {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.getThenInsertIfNew?_snd_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α fun (x : α) => β} (h : m.WF) {a : α} {b : β} :
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 : β} :