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: proof that all hash map operations preserve WFImp to show WF.out : WF → WFImp

@[simp]

theorem Std.DHashMap.Internal.toListModel_replicate_nil {α : Type u} {β : α → Type v} {c : Nat} :

toListModel (Array.replicate c AssocList.nil) = []

source

@[simp]

theorem Std.DHashMap.Internal.computeSize_eq {α : Type u} {β : α → Type v} {buckets : Array (AssocList α β)} :

computeSize buckets = (toListModel buckets).length

source

theorem Std.DHashMap.Internal.Raw.equiv_iff_toListModel_perm {α : Type u} {β : α → Type v} {m₁ m₂ : Raw α β} :

m₁.Equiv m₂ ↔ (toListModel m₁.buckets).Perm (toListModel m₂.buckets)

source

theorem Std.DHashMap.Internal.Raw.size_eq_length {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : WFImp m) :

m.size = (toListModel m.buckets).length

source

theorem Std.DHashMap.Internal.Raw.isEmpty_eq_isEmpty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : WFImp m) :

m.isEmpty = (toListModel m.buckets).isEmpty

source

theorem Std.DHashMap.Internal.Raw.fold_eq {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :

Raw.fold f init l = Array.foldl (fun (acc : γ) (l : AssocList α β) => AssocList.foldl f acc l) init l.buckets

source

theorem Std.DHashMap.Internal.Raw.fold_cons_apply {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :

Raw.fold (fun (acc : List γ) (k : α) (v : β k) => f k v :: acc) acc l = List.map (fun (p : (a : α) × β a) => f p.fst p.snd) (toListModel l.buckets).reverse ++ acc

source

theorem Std.DHashMap.Internal.Raw.fold_cons {α : Type u} {β : α → Type v} {l : Raw α β} {acc : List ((a : α) × β a)} :

Raw.fold (fun (acc : List ((a : α) × β a)) (k : α) (v : β k) => ⟨k, v⟩ :: acc) acc l = (toListModel l.buckets).reverse ++ acc

source

theorem Std.DHashMap.Internal.Raw.fold_cons_key {α : Type u} {β : α → Type v} {l : Raw α β} {acc : List α} :

Raw.fold (fun (acc : List α) (k : α) (x : β k) => k :: acc) acc l = Internal.List.keys (toListModel l.buckets).reverse ++ acc

source

theorem Std.DHashMap.Internal.Raw.foldRev_eq {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :

Raw.Internal.foldRev f init l = Array.foldr (fun (l : AssocList α β) (acc : γ) => AssocList.foldr (fun (a : α) (b : β a) (g : γ) => f g a b) acc l) init l.buckets

source

theorem Std.DHashMap.Internal.Raw.foldRev_cons_apply {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :

Raw.Internal.foldRev (fun (acc : List γ) (k : α) (v : β k) => f k v :: acc) acc l = List.map (fun (p : (a : α) × β a) => f p.fst p.snd) (toListModel l.buckets) ++ acc

source

theorem Std.DHashMap.Internal.Raw.fold_push_apply {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {acc : Array γ} (f : (a : α) → β a → γ) :

Raw.fold (fun (acc : Array γ) (k : α) (v : β k) => acc.push (f k v)) acc l = acc ++ Array.map (fun (p : (a : α) × β a) => f p.fst p.snd) (toListModel l.buckets).toArray

source

theorem Std.DHashMap.Internal.Raw.foldRev_cons {α : Type u} {β : α → Type v} {l : Raw α β} {acc : List ((a : α) × β a)} :

Raw.Internal.foldRev (fun (acc : List ((a : α) × β a)) (k : α) (v : β k) => ⟨k, v⟩ :: acc) acc l = toListModel l.buckets ++ acc

source

theorem Std.DHashMap.Internal.Raw.foldRev_cons_mk {α : Type u} {β : Type v} {l : Raw α fun (x : α) => β} {acc : List (α × β)} :

Raw.Internal.foldRev (fun (acc : List (α × β)) (k : α) (v : β) => (k, v) :: acc) acc l = List.map (fun (x : (_ : α) × β) => match x with | ⟨k, v⟩ => (k, v)) (toListModel l.buckets) ++ acc

source

theorem Std.DHashMap.Internal.Raw.foldRev_cons_key {α : Type u} {β : α → Type v} {l : Raw α β} {acc : List α} :

Raw.Internal.foldRev (fun (acc : List α) (k : α) (x : β k) => k :: acc) acc l = Internal.List.keys (toListModel l.buckets) ++ acc

source

theorem Std.DHashMap.Internal.Raw.foldRev_cons_value {α : Type u} {β : Type v} {l : Raw α fun (x : α) => β} {acc : List β} :

Raw.Internal.foldRev (fun (acc : List β) (x : α) (v : β) => v :: acc) acc l = Internal.List.values (toListModel l.buckets) ++ acc

source

theorem Std.DHashMap.Internal.Raw.fold_push {α : Type u} {β : α → Type v} {l : Raw α β} {acc : Array ((a : α) × β a)} :

Raw.fold (fun (acc : Array ((a : α) × β a)) (k : α) (v : β k) => acc.push ⟨k, v⟩) acc l = acc ++ (toListModel l.buckets).toArray

source

theorem Std.DHashMap.Internal.Raw.fold_push_mk {α : Type u} {β : Type v} {l : Raw α fun (x : α) => β} {acc : Array (α × β)} :

Raw.fold (fun (acc : Array (α × β)) (k : α) (v : β) => acc.push (k, v)) acc l = acc ++ (List.map (fun (x : (_ : α) × β) => match x with | ⟨k, v⟩ => (k, v)) (toListModel l.buckets)).toArray

source

theorem Std.DHashMap.Internal.Raw.fold_push_key {α : Type u} {β : α → Type v} {l : Raw α β} {acc : Array α} :

Raw.fold (fun (acc : Array α) (k : α) (x : β k) => acc.push k) acc l = acc ++ (Internal.List.keys (toListModel l.buckets)).toArray

source

theorem Std.DHashMap.Internal.Raw.foldM_eq_foldlM_toListModel {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ} {b : Raw α β} :

Raw.foldM f init b = List.foldlM (fun (a : δ) (b : (a : α) × β a) => f a b.fst b.snd) init (toListModel b.buckets)

source

theorem Std.DHashMap.Internal.Raw.fold_induction {α : Type u} {β : α → Type v} {δ : Type w} {f : δ → (a : α) → β a → δ} {init : δ} {b : Raw α β} {P : δ → Prop} (base : P init) (step : ∀ (acc : δ) (a : α) (b : β a), P acc → P (f acc a b)) :

P (Raw.fold f init b)

source

theorem Std.DHashMap.Internal.Raw.fold_eq_foldl_toListModel {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :

Raw.fold f init l = List.foldl (fun (a : γ) (b : (a : α) × β a) => f a b.fst b.snd) init (toListModel l.buckets)

source

theorem Std.DHashMap.Internal.Raw.foldRevM_eq_foldrM_toListModel {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ} {b : Raw α β} :

Raw.Internal.foldRevM f init b = List.foldrM (fun (a : (a : α) × β a) (b : δ) => f b a.fst a.snd) init (toListModel b.buckets)

source

theorem Std.DHashMap.Internal.Raw.foldRev_eq_foldr_toListModel {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :

Raw.Internal.foldRev f init l = List.foldr (fun (a : (a : α) × β a) (b : γ) => f b a.fst a.snd) init (toListModel l.buckets)

source

theorem Std.DHashMap.Internal.Raw.toList_eq_toListModel {α : Type u} {β : α → Type v} {m : Raw α β} :

m.toList = toListModel m.buckets

source

theorem Std.DHashMap.Internal.Raw.Const.toList_eq_toListModel_map {α : Type u} {β : Type v} {m : Raw α fun (x : α) => β} :

Raw.Const.toList m = List.map (fun (x : (_ : α) × β) => match x with | ⟨k, v⟩ => (k, v)) (toListModel m.buckets)

source

theorem Std.DHashMap.Internal.Raw.toArray_eq_toArray_toListModel {α : Type u} {β : α → Type v} {m : Raw α β} :

m.toArray = (toListModel m.buckets).toArray

source

theorem Std.DHashMap.Internal.Raw.Const.toArray_eq_toArray_map_toListModel {α : Type u} {β : Type v} {m : Raw α fun (x : α) => β} :

Raw.Const.toArray m = (List.map (fun (x : (_ : α) × β) => match x with | ⟨k, v⟩ => (k, v)) (toListModel m.buckets)).toArray

source

theorem Std.DHashMap.Internal.Raw.keys_eq_keys_toListModel {α : Type u} {β : α → Type v} {m : Raw α β} :

m.keys = Internal.List.keys (toListModel m.buckets)

source

theorem Std.DHashMap.Internal.Raw.values_eq_values_toListModel {α : Type u} {β : Type v} {m : Raw α fun (x : α) => β} :

m.values = Internal.List.values (toListModel m.buckets)

source

theorem Std.DHashMap.Internal.Raw.keysArray_eq_toArray_keys_toListModel {α : Type u} {β : α → Type v} {m : Raw α β} :

m.keysArray = (Internal.List.keys (toListModel m.buckets)).toArray

source

theorem Std.DHashMap.Internal.Raw.forM_eq_forM_toListModel {α : Type u} {β : α → Type v} {l : Raw α β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → m PUnit} :

Raw.forM f l = (toListModel l.buckets).forM fun (a : (a : α) × β a) => f a.fst a.snd

source

theorem Std.DHashMap.Internal.Raw.forIn_eq_forIn_toListModel {α : Type u} {β : α → Type v} {δ : Type w} {l : Raw α β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ} :

Raw.forIn f init l = ForIn.forIn (toListModel l.buckets) init fun (a : (a : α) × β a) (d : δ) => f a.fst a.snd d

source

theorem Std.DHashMap.Internal.Raw.all_eq_all_toListModel {α : Type u} {β : α → Type v} {p : (a : α) → β a → Bool} {m : Raw α β} :

m.all p = (toListModel m.buckets).all fun (x : (a : α) × β a) => p x.fst x.snd

Raw₀.empty #

source

@[simp]

theorem Std.DHashMap.Internal.Raw₀.toListModel_buckets_emptyWithCapacity {α : Type u} {β : α → Type v} {c : Nat} :

toListModel (emptyWithCapacity c).val.buckets = []

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_emptyWithCapacity {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {c : Nat} :

Raw.WFImp (emptyWithCapacity c).val

source

theorem Std.DHashMap.Internal.Raw₀.isHashSelf_reinsertAux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (data : { d : Array (AssocList α β) // 0 < d.size }) (a : α) (b : β a) (h : IsHashSelf data.val) :

IsHashSelf (reinsertAux hash data a b).val

expandIfNecessary #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_reinsertAux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] (data : { d : Array (AssocList α β) // 0 < d.size }) (a : α) (b : β a) :

(toListModel (reinsertAux hash data a b).val).Perm (⟨a, b⟩ :: toListModel data.val)

source

theorem Std.DHashMap.Internal.Raw₀.isHashSelf_foldl_reinsertAux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (l : List ((a : α) × β a)) (target : { d : Array (AssocList α β) // 0 < d.size }) :

IsHashSelf target.val → IsHashSelf (List.foldl (fun (acc : { d : Array (AssocList α β) // 0 < d.size }) (p : (a : α) × β a) => reinsertAux hash acc p.fst p.snd) target l).val

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_foldl_reinsertAux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] (l : List ((a : α) × β a)) (target : { d : Array (AssocList α β) // 0 < d.size }) :

(toListModel (List.foldl (fun (acc : { d : Array (AssocList α β) // 0 < d.size }) (p : (a : α) × β a) => reinsertAux hash acc p.fst p.snd) target l).val).Perm (l ++ toListModel target.val)

source

theorem Std.DHashMap.Internal.Raw₀.isHashSelf_expand {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulHashable α] [EquivBEq α] {buckets : { d : Array (AssocList α β) // 0 < d.size }} :

IsHashSelf (expand buckets).val

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_expand {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] {buckets : { d : Array (AssocList α β) // 0 < d.size }} :

(toListModel (expand buckets).val).Perm (toListModel buckets.val)

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_expandIfNecessary {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] (m : Raw₀ α β) :

(toListModel m.expandIfNecessary.val.buckets).Perm (toListModel m.val.buckets)

source

@[simp]

theorem Std.DHashMap.Internal.Raw₀.size_expandIfNecessary {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} :

m.expandIfNecessary.val.size = m.val.size

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_expandIfNecessary {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) :

Raw.WFImp m.expandIfNecessary.val

Access operations #

source

theorem Std.DHashMap.Internal.Raw₀.containsₘ_eq_containsKey {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :

m.containsₘ a = Internal.List.containsKey a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.contains_eq_containsKey {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :

m.contains a = Internal.List.containsKey a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.get?ₘ_eq_getValueCast? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :

m.get?ₘ a = Internal.List.getValueCast? a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.get?_eq_getValueCast? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :

m.get? a = Internal.List.getValueCast? a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.getₘ_eq_getValue {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {h : m.containsₘ a = true} :

m.getₘ a h = Internal.List.getValueCast a (toListModel m.val.buckets) ⋯

source

theorem Std.DHashMap.Internal.Raw₀.getEntryₘ_eq_getEntry {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {h : m.containsₘ a = true} :

m.getEntryₘ a h = Internal.List.getEntry a (toListModel m.val.buckets) ⋯

source

theorem Std.DHashMap.Internal.Raw₀.getEntry?ₘ_eq_getEntry? {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :

m.getEntry?ₘ a = Internal.List.getEntry? a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.get_eq_getValueCast {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {h : m.contains a = true} :

m.get a h = Internal.List.getValueCast a (toListModel m.val.buckets) ⋯

source

theorem Std.DHashMap.Internal.Raw₀.getEntry_eq_getEntry {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {h : m.contains a = true} :

m.getEntry a h = Internal.List.getEntry a (toListModel m.val.buckets) ⋯

source

theorem Std.DHashMap.Internal.Raw₀.getEntry?_eq_getEntry? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :

m.getEntry? a = Internal.List.getEntry? a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.getEntryDₘ_eq_getEntryD {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {fallback : (a : α) × β a} :

m.getEntryDₘ a fallback = Internal.List.getEntryD a fallback (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.getEntryD_eq_getEntryD {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {fallback : (a : α) × β a} :

m.getEntryD a fallback = Internal.List.getEntryD a fallback (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.getEntry!ₘ_eq_getEntry! {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} [Inhabited ((a : α) × β a)] :

m.getEntry!ₘ a = Internal.List.getEntry! a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.getEntry!_eq_getEntry! {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} [Inhabited ((a : α) × β a)] :

m.getEntry! a = Internal.List.getEntry! a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.get!ₘ_eq_getValueCast! {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} [Inhabited (β a)] :

m.get!ₘ a = Internal.List.getValueCast! a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.get!_eq_getValueCast! {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} [Inhabited (β a)] :

m.get! a = Internal.List.getValueCast! a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.getDₘ_eq_getValueCastD {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {fallback : β a} :

m.getDₘ a fallback = Internal.List.getValueCastD a (toListModel m.val.buckets) fallback

source

theorem Std.DHashMap.Internal.Raw₀.getD_eq_getValueCastD {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {fallback : β a} :

m.getD a fallback = Internal.List.getValueCastD a (toListModel m.val.buckets) fallback

source

theorem Std.DHashMap.Internal.Raw₀.getKey?ₘ_eq_getKey? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :

m.getKey?ₘ a = Internal.List.getKey? a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.getKey?_eq_getKey? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :

m.getKey? a = Internal.List.getKey? a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.getKeyₘ_eq_getKey {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {h : m.contains a = true} :

m.getKeyₘ a h = Internal.List.getKey a (toListModel m.val.buckets) ⋯

source

theorem Std.DHashMap.Internal.Raw₀.getKey_eq_getKey {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {h : m.contains a = true} :

m.getKey a h = Internal.List.getKey a (toListModel m.val.buckets) ⋯

source

theorem Std.DHashMap.Internal.Raw₀.getKey!ₘ_eq_getKey! {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :

m.getKey!ₘ a = Internal.List.getKey! a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.getKey!_eq_getKey! {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :

m.getKey! a = Internal.List.getKey! a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.getKeyDₘ_eq_getKeyD {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a fallback : α} :

m.getKeyDₘ a fallback = Internal.List.getKeyD a (toListModel m.val.buckets) fallback

source

theorem Std.DHashMap.Internal.Raw₀.getKeyD_eq_getKeyD {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a fallback : α} :

m.getKeyD a fallback = Internal.List.getKeyD a (toListModel m.val.buckets) fallback

source

theorem Std.DHashMap.Internal.Raw₀.Const.get?ₘ_eq_getValue? {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} :

get?ₘ m a = Internal.List.getValue? a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.Const.get?_eq_getValue? {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} :

get? m a = Internal.List.getValue? a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.Const.getₘ_eq_getValue {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} {h : m.containsₘ a = true} :

getₘ m a h = Internal.List.getValue a (toListModel m.val.buckets) ⋯

source

theorem Std.DHashMap.Internal.Raw₀.Const.get_eq_getValue {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} {h : m.contains a = true} :

get m a h = Internal.List.getValue a (toListModel m.val.buckets) ⋯

source

theorem Std.DHashMap.Internal.Raw₀.Const.get!ₘ_eq_getValue! {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] [Inhabited β] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} :

get!ₘ m a = Internal.List.getValue! a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.Const.get!_eq_getValue! {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] [Inhabited β] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} :

get! m a = Internal.List.getValue! a (toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.Const.getDₘ_eq_getValueD {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} {fallback : β} :

getDₘ m a fallback = Internal.List.getValueD a (toListModel m.val.buckets) fallback

source

theorem Std.DHashMap.Internal.Raw₀.Const.getD_eq_getValueD {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} {fallback : β} :

getD m a fallback = Internal.List.getValueD a (toListModel m.val.buckets) fallback

`replaceₘ` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_replaceₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (b : β a) :

(toListModel (m.replaceₘ a b).val.buckets).Perm (Internal.List.replaceEntry a b (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.isHashSelf_replaceₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (b : β a) :

IsHashSelf (m.replaceₘ a b).val.buckets

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_replaceₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (b : β a) :

Raw.WFImp (m.replaceₘ a b).val

`insertₘ` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_consₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (b : β a) :

(toListModel (m.consₘ a b).val.buckets).Perm (⟨a, b⟩ :: toListModel m.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.isHashSelf_consₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (b : β a) :

IsHashSelf (m.consₘ a b).val.buckets

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_consₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (b : β a) (hc : m.containsₘ a = false) :

Raw.WFImp (m.consₘ a b).val

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_insertₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :

(toListModel (m.insertₘ a b).val.buckets).Perm (Internal.List.insertEntry a b (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_insertₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :

Raw.WFImp (m.insertₘ a b).val

`insert` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_insert {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :

(toListModel (m.insert a b).val.buckets).Perm (Internal.List.insertEntry a b (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_insert {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :

Raw.WFImp (m.insert a b).val

`alter` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_updateBucket_alter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :

(toListModel (updateBucket m.val.buckets ⋯ a (AssocList.alter a f))).Perm (Internal.List.alterKey a f (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.isHashSelf_updateBucket_alter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :

IsHashSelf (updateBucket m.val.buckets ⋯ a (AssocList.alter a f))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_updateBucket_alter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :

Raw.WFImp (withComputedSize (updateBucket m.val.buckets ⋯ a (AssocList.alter a f)))

source

theorem Std.DHashMap.Internal.Raw₀.isHashSelf_alterₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (f : Option (β a) → Option (β a)) :

IsHashSelf (m.alterₘ a f).val.buckets

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_alterₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :

(toListModel (m.alterₘ a f).val.buckets).Perm (Internal.List.alterKey a f (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_alter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :

(toListModel (m.alter a f).val.buckets).Perm (Internal.List.alterKey a f (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_alterₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :

Raw.WFImp (m.alterₘ a f).val

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_alter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :

Raw.WFImp (m.alter a f).val

source

theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_updateBucket_alter {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :

(toListModel (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f))).Perm (Internal.List.Const.alterKey a f (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.Const.isHashSelf_updateBucket_alter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :

IsHashSelf (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f))

source

theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_updateBucket_alter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :

Raw.WFImp (withComputedSize (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f)))

source

theorem Std.DHashMap.Internal.Raw₀.Const.isHashSelf_alterₘ {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : Raw.WFImp m.val) (a : α) (f : Option β → Option β) :

IsHashSelf (alterₘ m a f).val.buckets

source

theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_alterₘ {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :

(toListModel (alterₘ m a f).val.buckets).Perm (Internal.List.Const.alterKey a f (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_alter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :

(toListModel (alter m a f).val.buckets).Perm (Internal.List.Const.alterKey a f (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_alterₘ {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :

Raw.WFImp (alterₘ m a f).val

source

theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_alter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :

Raw.WFImp (alter m a f).val

`modify` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_modify {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : β a → β a} :

(toListModel (m.modify a f).val.buckets).Perm (Internal.List.modifyKey a f (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_modifyₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : β a → β a} :

Raw.WFImp (m.modifyₘ a f).val

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_modify {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : β a → β a} :

Raw.WFImp (m.modify a f).val

source

theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_modify {α : Type u} {β : Type v} {m : Raw₀ α fun (x : α) => β} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (h : Raw.WFImp m.val) {a : α} {f : β → β} :

(toListModel (modify m a f).val.buckets).Perm (Internal.List.Const.modifyKey a f (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_modifyₘ {α : Type u} {β : Type v} {m : Raw₀ α fun (x : α) => β} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (h : Raw.WFImp m.val) {a : α} {f : β → β} :

Raw.WFImp (modifyₘ m a f).val

source

theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_modify {α : Type u} {β : Type v} {m : Raw₀ α fun (x : α) => β} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (h : Raw.WFImp m.val) {a : α} {f : β → β} :

Raw.WFImp (modify m a f).val

`containsThenInsert` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_containsThenInsert {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :

(toListModel (m.containsThenInsert a b).snd.val.buckets).Perm (Internal.List.insertEntry a b (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_containsThenInsert {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :

Raw.WFImp (m.containsThenInsert a b).snd.val

`insertIfNewₘ` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_insertIfNewₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :

(toListModel (m.insertIfNewₘ a b).val.buckets).Perm (Internal.List.insertEntryIfNew a b (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_insertIfNewₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :

Raw.WFImp (m.insertIfNewₘ a b).val

`insertIfNew` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_insertIfNew {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :

(toListModel (m.insertIfNew a b).val.buckets).Perm (Internal.List.insertEntryIfNew a b (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_insertIfNew {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :

Raw.WFImp (m.insertIfNew a b).val

`containsThenInsertIfNew` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_containsThenInsertIfNew {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :

(toListModel (m.containsThenInsertIfNew a b).snd.val.buckets).Perm (Internal.List.insertEntryIfNew a b (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_containsThenInsertIfNew {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :

Raw.WFImp (m.containsThenInsertIfNew a b).snd.val

`getThenInsertIfNew?` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_getThenInsertIfNew? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α} {b : β a} (h : Raw.WFImp m.val) :

(toListModel (m.getThenInsertIfNew? a b).snd.val.buckets).Perm (Internal.List.insertEntryIfNew a b (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_getThenInsertIfNew? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α} {b : β a} (h : Raw.WFImp m.val) :

Raw.WFImp (m.getThenInsertIfNew? a b).snd.val

`Const.getThenInsertIfNew?` #

source

theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_getThenInsertIfNew? {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} {a : α} {b : β} (h : Raw.WFImp m.val) :

(toListModel (getThenInsertIfNew? m a b).snd.val.buckets).Perm (Internal.List.insertEntryIfNew a b (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_getThenInsertIfNew? {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} {a : α} {b : β} (h : Raw.WFImp m.val) :

Raw.WFImp (getThenInsertIfNew? m a b).snd.val

`eraseₘ` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_eraseₘaux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (a : α) (h : Raw.WFImp m.val) :

(toListModel (m.eraseₘaux a).val.buckets).Perm (Internal.List.eraseKey a (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.isHashSelf_eraseₘaux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (a : α) (h : Raw.WFImp m.val) :

IsHashSelf (m.eraseₘaux a).val.buckets

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_eraseₘaux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (a : α) (h : Raw.WFImp m.val) (h' : m.containsₘ a = true) :

Raw.WFImp (m.eraseₘaux a).val

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_perm_eraseKey_of_containsₘ_eq_false {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (a : α) (h : Raw.WFImp m.val) (h' : m.containsₘ a = false) :

(toListModel m.val.buckets).Perm (Internal.List.eraseKey a (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_eraseₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {a : α} (h : Raw.WFImp m.val) :

(toListModel (m.eraseₘ a).val.buckets).Perm (Internal.List.eraseKey a (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_eraseₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {a : α} (h : Raw.WFImp m.val) :

Raw.WFImp (m.eraseₘ a).val

`erase` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_erase {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {a : α} (h : Raw.WFImp m.val) :

(toListModel (m.erase a).val.buckets).Perm (Internal.List.eraseKey a (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_erase {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {a : α} (h : Raw.WFImp m.val) :

Raw.WFImp (m.erase a).val

`filterₘ` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_filterₘ {α : Type u} {β : α → Type v} {m : Raw₀ α β} {f : (a : α) → β a → Bool} :

(toListModel (m.filterₘ f).val.buckets).Perm (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.isHashSelf_filterₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → Bool} (h : Raw.WFImp m.val) :

IsHashSelf (m.filterₘ f).val.buckets

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_filterₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → Bool} (h : Raw.WFImp m.val) :

Raw.WFImp (m.filterₘ f).val

`filter` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_filter {α : Type u} {β : α → Type v} {m : Raw₀ α β} {f : (a : α) → β a → Bool} :

(toListModel (filter f m).val.buckets).Perm (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_filter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → Bool} (h : Raw.WFImp m.val) :

Raw.WFImp (filter f m).val

`insertListₘ` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_insertListₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.val) :

(toListModel (m.insertListₘ l).val.buckets).Perm (Internal.List.insertList (toListModel m.val.buckets) l)

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_eraseListₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {l : List α} (h : Raw.WFImp m.val) :

(toListModel (m.eraseListₘ l).val.buckets).Perm (Internal.List.eraseList (toListModel m.val.buckets) l)

`insertListₘ` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_insertListIfNewₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.val) :

(toListModel (m.insertListIfNewₘ l).val.buckets).Perm (Internal.List.insertListIfNew (toListModel m.val.buckets) l)

`unionₘ` #

source

theorem Std.DHashMap.Internal.Raw₀.insertMany_eq_insertListₘ_toListModel {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m m₂ : Raw₀ α β) :

(m.insertMany m₂.val).val = m.insertListₘ (toListModel m₂.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.insertMany_array_eq_insertMany_toList {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m : Raw₀ α β) (a : Array ((k : α) × β k)) :

m.insertMany a = m.insertMany a.toList

source

theorem Std.DHashMap.Internal.Raw₀.Const.insertMany_array_eq_insertMany_toList {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) (a : Array (α × β)) :

insertMany m a = insertMany m a.toList

source

theorem Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_array_eq_insertManyIfNewUnit_toList {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) (a : Array α) :

insertManyIfNewUnit m a = insertManyIfNewUnit m a.toList

source

theorem Std.DHashMap.Internal.Raw₀.insertManyIfNew_eq_insertListIfNewₘ_toListModel {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m m₂ : Raw₀ α β) :

(m.insertManyIfNew m₂.val).val = m.insertListIfNewₘ (toListModel m₂.val.buckets)

source

theorem Std.DHashMap.Internal.Raw₀.union_eq_unionₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m₁ m₂ : Raw₀ α β) :

m₁.union m₂ = m₁.unionₘ m₂

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_unionₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Raw₀ α β} (h₁ : Raw.WFImp m₁.val) (h₂ : Raw.WFImp m₂.val) :

(toListModel (m₁.unionₘ m₂).val.buckets).Perm (Internal.List.insertList (toListModel m₁.val.buckets) (toListModel m₂.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_inter {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m₁ m₂ : Raw α β} {h₁ : 0 < m₁.buckets.size} {h₂ : 0 < m₂.buckets.size} (wh₁ : Raw.WFImp m₁) :

Raw.WFImp (inter ⟨m₁, h₁⟩ ⟨m₂, h₂⟩).val

source

theorem Std.DHashMap.Internal.Raw.WF.out {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [i₁ : EquivBEq α] [i₂ : LawfulHashable α] {m : Raw α β} (h : m.WF) :

WFImp m

`filterMapₘ` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_filterMapₘ {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} :

(toListModel (m.filterMapₘ f).val.buckets).Perm (List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : δ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.isHashSelf_filterMapₘ {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.val) :

IsHashSelf (m.filterMapₘ f).val.buckets

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_filterMapₘ {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.val) :

Raw.WFImp (m.filterMapₘ f).val

`filterMap` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_filterMap {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} :

(toListModel (filterMap f m).val.buckets).Perm (List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : δ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_filterMap {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.val) :

Raw.WFImp (filterMap f m).val

source

theorem Std.DHashMap.Internal.Raw₀.wf_filterMap₀ {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Raw₀ α β} (h : m.val.WF) {f : (a : α) → β a → Option (δ a)} :

(filterMap f m).val.WF

source

theorem Std.DHashMap.Internal.Raw₀.filterMap_eq_filter {α : Type u} {β : α → Type v} {m : Raw₀ α β} {f : (a : α) → β a → Bool} :

filterMap (fun (k : α) => Option.guard fun (v : β k) => f k v) m = filter f m

source

theorem Std.DHashMap.Internal.Raw₀.filterMap_eq_map {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {γ : α → Type w} (m : Raw₀ α β) (f : (a : α) → β a → γ a) (h : m.val.WF) :

filterMap (fun (k : α) (v : β k) => some (f k v)) m = map f m

`mapₘ` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_mapₘ {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Raw₀ α β} {f : (a : α) → β a → δ a} :

(toListModel (m.mapₘ f).val.buckets).Perm (List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.isHashSelf_mapₘ {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → δ a} (h : Raw.WFImp m.val) :

IsHashSelf (m.mapₘ f).val.buckets

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_mapₘ {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → δ a} (h : Raw.WFImp m.val) :

Raw.WFImp (m.mapₘ f).val

`map` #

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_map {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Raw₀ α β} {f : (a : α) → β a → δ a} :

(toListModel (map f m).val.buckets).Perm (List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) (toListModel m.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_map {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → δ a} (h : Raw.WFImp m.val) :

Raw.WFImp (map f m).val

source

theorem Std.DHashMap.Internal.Raw₀.wf_map₀ {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Raw₀ α β} (h : m.val.WF) {f : (a : α) → β a → δ a} :

(map f m).val.WF

`insertMany` #

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_insertMany {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw₀ α β} {l : ρ} (h : Raw.WFImp m.val) :

Raw.WFImp (m.insertMany l).val.val

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_insertMany_list {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.val) :

(toListModel (m.insertMany l).val.val.buckets).Perm (Internal.List.insertList (toListModel m.val.buckets) l)

source

theorem Std.DHashMap.Internal.Raw₀.insertMany_list_eq_foldl {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} :

(m.insertMany l).val = List.foldl (fun (a : Raw₀ α β) (b : (a : α) × β a) => a.insert b.fst b.snd) m l

`eraseMany` #

source

theorem Std.DHashMap.Internal.Raw₀.WF.eraseManyEntries {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw α β} {l : ρ} (h : m.WF) :

(m.eraseManyEntries l).WF

source

theorem Std.DHashMap.Internal.Raw₀.wf_insertMany₀ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw α β} {h : 0 < m.buckets.size} {l : ρ} (h' : m.WF) :

(insertMany ⟨m, h⟩ l).val.val.WF

source

theorem Std.DHashMap.Internal.Raw₀.wf_eraseMany₀ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw α β} {h : 0 < m.buckets.size} {l : ρ} (h' : m.WF) :

(eraseManyEntries ⟨m, h⟩ l).val.val.WF

source

theorem Std.DHashMap.Internal.Raw₀.eraseMany_eq_eraseListₘ_toListModel {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m m₂ : Raw₀ α β) :

(m.eraseManyEntries m₂.val).val = m.eraseListₘ (List.map (fun (x : (a : α) × β a) => x.fst) (toListModel m₂.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_diffₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Raw₀ α β} (h₁ : Raw.WFImp m₁.val) (h₂ : Raw.WFImp m₂.val) :

(toListModel (m₁.diffₘ m₂).val.buckets).Perm (List.filter (fun (k : (a : α) × β a) => !(List.map Sigma.fst (toListModel m₂.val.buckets)).contains k.fst) (toListModel m₁.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.diff_eq_diffₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m₁ m₂ : Raw₀ α β) :

m₁.diff m₂ = m₁.diffₘ m₂

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_diff {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Raw₀ α β} (h₁ : Raw.WFImp m₁.val) (h₂ : Raw.WFImp m₂.val) :

(toListModel (m₁.diff m₂).val.buckets).Perm (List.filter (fun (k : (a : α) × β a) => !(List.map Sigma.fst (toListModel m₂.val.buckets)).contains k.fst) (toListModel m₁.val.buckets))

source

theorem Std.DHashMap.Internal.Raw₀.wf_diff₀ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Raw α β} {h₁ : 0 < m₁.buckets.size} {h₂ : 0 < m₂.buckets.size} (h'₁ : m₁.WF) :

(diff ⟨m₁, h₁⟩ ⟨m₂, h₂⟩).val.WF

`insertManyIfNew` #

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_insertManyIfNew {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw₀ α β} {l : ρ} (h : Raw.WFImp m.val) :

Raw.WFImp (m.insertManyIfNew l).val.val

source

theorem Std.DHashMap.Internal.Raw₀.wf_insertManyIfNew₀ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw α β} {h : 0 < m.buckets.size} {l : ρ} (h' : m.WF) :

(insertManyIfNew ⟨m, h⟩ l).val.val.WF

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_insertManyIfNew_list {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.val) :

(toListModel (m.insertManyIfNew l).val.val.buckets).Perm (Internal.List.insertListIfNew (toListModel m.val.buckets) l)

source

theorem Std.DHashMap.Internal.Raw₀.insertManyIfNew_list_eq_foldl {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} :

(m.insertManyIfNew l).val = List.foldl (fun (a : Raw₀ α β) (b : (a : α) × β a) => a.insertIfNew b.fst b.snd) m l

`union` #

source

theorem Std.DHashMap.Internal.Raw₀.wf_union₀ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Raw α β} {h₁ : 0 < m₁.buckets.size} {h₂ : 0 < m₂.buckets.size} (h'₁ : m₁.WF) (h'₂ : m₂.WF) :

(union ⟨m₁, h₁⟩ ⟨m₂, h₂⟩).val.WF

source

theorem Std.DHashMap.Internal.Raw₀.toListModel_union {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Raw₀ α β} (h₁ : Raw.WFImp m₁.val) (h₂ : Raw.WFImp m₂.val) :

(toListModel (m₁.union m₂).val.buckets).Perm (Internal.List.insertList (toListModel m₁.val.buckets) (toListModel m₂.val.buckets))

`inter` #

source

theorem Std.DHashMap.Internal.Raw₀.wfImp_interSmallerFnₘ {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (m₁ m₂ : Raw₀ α β) (hm₂ : Raw.WFImp m₂.val) (k : α) :

Raw.WFImp (m₁.interSmallerFnₘ m₂ k).val

source

def Std.DHashMap.Internal.Raw₀.interSmallerₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m₁ : Raw₀ α β) (m₂ : Raw α β) :

Raw₀ α β

Internal implementation detail of the hash map

Equations

m₁.interSmallerₘ m₂ = Std.DHashMap.Raw.fold (fun (sofar : Std.DHashMap.Internal.Raw₀ α β) (k : α) (x : β k) => m₁.interSmallerFnₘ sofar k) Std.DHashMap.Internal.Raw₀.emptyWithCapacity m₂

Instances For

source

theorem Std.DHashMap.Internal.Raw₀.interSmaller_eq_interSmallerₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m₁ : Raw₀ α β) (m₂ : Raw α β) :

m₁.interSmaller m₂ = m₁.interSmallerₘ m₂

source

theorem Std.DHashMap.Internal.Raw₀.foldl_perm_cong {α : Type u} {β : α → Type v} [BEq α] {init₁ init₂ l : List ((a : α) × β a)} {f : List ((a : α) × β a) → (a : α) × β a → List ((a : α) × β a)} (h₁ : init₁.Perm init₂) (h₂ : ∀ (h : (a : α) × β a) (l₁ l₂ : List ((a : α) × β a)), Internal.List.DistinctKeys l₁ → l₁.Perm l₂ → (f l₁ h).Perm (f l₂ h) ∧ Internal.List.DistinctKeys (f l₁ h)) (h₃ : Internal.List.DistinctKeys init₁) :

(List.foldl f init₁ l).Perm (List.foldl f init₂ l)

source