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: Connecting operations on `AssocList` to operations defined in `List.Associative`

source
@[simp]
theorem Std.DHashMap.Internal.AssocList.toList_nil {α : Type u} {β : α → Type v} :
nil.toList = []
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.toList_cons {α : Type u} {β : α → Type v} {l : AssocList α β} {a : α} {b : β a} :
(cons a b l).toList = ⟨a, b⟩ :: l.toList
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.foldl_eq {α : Type u} {β : α → Type v} {δ : Type w} {f : δ → (a : α) → β a → δ} {init : δ} {l : AssocList α β} :
foldl f init l = List.foldl (fun (d : δ) (p : (a : α) × β a) => f d p.fst p.snd) init l.toList
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.length_eq {α : Type u} {β : α → Type v} {l : AssocList α β} :
l.length = l.toList.length
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.get?_eq {α : Type u} {β : Type v} [BEq α] {l : AssocList α fun (x : α) => β} {a : α} :
get? a l = Internal.List.getValue? a l.toList
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.getCast?_eq {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : AssocList α β} {a : α} :
getCast? a l = Internal.List.getValueCast? a l.toList
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.contains_eq {α : Type u} {β : α → Type v} [BEq α] {l : AssocList α β} {a : α} :
contains a l = Internal.List.containsKey a l.toList
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.getCast_eq {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : AssocList α β} {a : α} {h : contains a l = true} :
getCast a l h = Internal.List.getValueCast a l.toList ⋯
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.get_eq {α : Type u} {β : Type v} [BEq α] {l : AssocList α fun (x : α) => β} {a : α} {h : contains a l = true} :
get a l h = Internal.List.getValue a l.toList ⋯
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.getCastD_eq {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : AssocList α β} {a : α} {fallback : β a} :
getCastD a fallback l = Internal.List.getValueCastD a l.toList fallback
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.getD_eq {α : Type u} {β : Type v} [BEq α] {l : AssocList α fun (x : α) => β} {a : α} {fallback : β} :
getD a fallback l = Internal.List.getValueD a l.toList fallback
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.panicWithPosWithDecl_eq {α : Type u} [Inhabited α] {modName declName : String} {line col : Nat} {msg : String} :
panicWithPosWithDecl modName declName line col msg = default
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.getCast!_eq {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : AssocList α β} {a : α} [Inhabited (β a)] :
getCast! a l = Internal.List.getValueCast! a l.toList
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.get!_eq {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : AssocList α fun (x : α) => β} {a : α} :
get! a l = Internal.List.getValue! a l.toList
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.getKey?_eq {α : Type u} {β : α → Type v} [BEq α] {l : AssocList α β} {a : α} :
getKey? a l = Internal.List.getKey? a l.toList
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.getKey_eq {α : Type u} {β : α → Type v} [BEq α] {l : AssocList α β} {a : α} {h : contains a l = true} :
getKey a l h = Internal.List.getKey a l.toList ⋯
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.getKeyD_eq {α : Type u} {β : α → Type v} [BEq α] {l : AssocList α β} {a fallback : α} :
getKeyD a fallback l = Internal.List.getKeyD a l.toList fallback
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.getKey!_eq {α : Type u} {β : α → Type v} [BEq α] [Inhabited α] {l : AssocList α β} {a : α} :
getKey! a l = Internal.List.getKey! a l.toList
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.toList_replace {α : Type u} {β : α → Type v} [BEq α] {l : AssocList α β} {a : α} {b : β a} :
(replace a b l).toList = Internal.List.replaceEntry a b l.toList
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.toList_erase {α : Type u} {β : α → Type v} [BEq α] {l : AssocList α β} {a : α} :
(erase a l).toList = Internal.List.eraseKey a l.toList
source
theorem Std.DHashMap.Internal.AssocList.toList_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} {f : (a : α) → β a → Option (γ a)} {l : AssocList α β} :
(filterMap f l).toList.Perm (List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l.toList)
source
theorem Std.DHashMap.Internal.AssocList.toList_map {α : Type u} {β : α → Type v} {γ : α → Type w} {f : (a : α) → β a → γ a} {l : AssocList α β} :
(map f l).toList.Perm (List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) l.toList)
source
theorem Std.DHashMap.Internal.AssocList.toList_filter {α : Type u} {β : α → Type v} {f : (a : α) → β a → Bool} {l : AssocList α β} :
(filter f l).toList.Perm (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l.toList)
source
theorem Std.DHashMap.Internal.AssocList.filterMap_eq_map {α : Type u} {β : α → Type v} {γ : α → Type w} {f : (a : α) → β a → γ a} {l : AssocList α β} :
filterMap (fun (k : α) (v : β k) => some (f k v)) l = map f l
source
theorem Std.DHashMap.Internal.AssocList.filterMap_eq_filter {α : Type u} {β : α → Type v} {f : (a : α) → β a → Bool} {l : AssocList α β} :
filterMap (fun (k : α) => Option.guard fun (v : β k) => f k v) l = filter f l
source
theorem Std.DHashMap.Internal.AssocList.toList_alter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} {l : AssocList α β} :
(alter a f l).toList.Perm (Internal.List.alterKey a f l.toList)
source
theorem Std.DHashMap.Internal.AssocList.modify_eq_alter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {f : β a → β a} {l : AssocList α β} :
modify a f l = alter a (fun (x : Option (β a)) => Option.map f x) l
source
theorem Std.DHashMap.Internal.AssocList.Const.toList_alter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {a : α} {f : Option β → Option β} {l : AssocList α fun (x : α) => β} :
(alter a f l).toList.Perm (Internal.List.Const.alterKey a f l.toList)
source
theorem Std.DHashMap.Internal.AssocList.Const.modify_eq_alter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {a : α} {f : β → β} {l : AssocList α fun (x : α) => β} :
modify a f l = alter a (fun (x : Option β) => Option.map f x) l
source
theorem Std.DHashMap.Internal.AssocList.foldl_apply {α : Type u} {β : α → Type v} {δ : Type w} {l : AssocList α β} {acc : List δ} (f : (a : α) → β a → δ) :
foldl (fun (acc : List δ) (k : α) (v : β k) => f k v :: acc) acc l = (List.map (fun (p : (a : α) × β a) => f p.fst p.snd) l.toList).reverse ++ acc
source
theorem Std.DHashMap.Internal.AssocList.foldr_apply {α : Type u} {β : α → Type v} {δ : Type w} {l : AssocList α β} {acc : List δ} (f : (a : α) → β a → δ) :
foldr (fun (k : α) (v : β k) (acc : List δ) => f k v :: acc) acc l = List.map (fun (p : (a : α) × β a) => f p.fst p.snd) l.toList ++ acc
source
theorem Std.DHashMap.Internal.AssocList.foldl_push_apply {α : Type u} {β : α → Type v} {δ : Type w} {l : AssocList α β} {acc : Array δ} (f : (a : α) → β a → δ) :
foldl (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) l.toList.toArray