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

@[simp]

theorem Std.DHashMap.Internal.AssocList.toList_nil {α : Type u} {β : α → Type v} : nil.toList = []

@[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

@[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

@[simp]

theorem Std.DHashMap.Internal.AssocList.length_eq {α : Type u} {β : α → Type v} {l : AssocList α β} : l.length = l.toList.length

@[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

@[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

@[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

@[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 ⋯

@[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 ⋯

@[simp]

theorem Std.DHashMap.Internal.AssocList.getEntry_eq {α : Type u} {β : α → Type v} [BEq α] {l : AssocList α β} {a : α} {h : contains a l = true} : getEntry a l h = Internal.List.getEntry a l.toList ⋯

@[simp]

theorem Std.DHashMap.Internal.AssocList.getEntry?_eq {α : Type u} {β : α → Type v} [BEq α] {l : AssocList α β} {a : α} : getEntry? a l = Internal.List.getEntry? a l.toList

@[simp]

theorem Std.DHashMap.Internal.AssocList.getEntryD_eq {α : Type u} {β : α → Type v} [BEq α] {l : AssocList α β} {a : α} {fallback : (a : α) × β a} : getEntryD a fallback l = Internal.List.getEntryD a fallback l.toList

@[simp]

theorem Std.DHashMap.Internal.AssocList.getEntry!_eq {α : Type u} {β : α → Type v} [BEq α] {l : AssocList α β} {a : α} [Inhabited ((a : α) × β a)] : getEntry! a l = Internal.List.getEntry! a l.toList

@[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

@[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

@[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

@[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

@[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

@[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

@[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 ⋯

@[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

@[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

@[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

@[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

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)

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)

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)

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

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

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)

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

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)

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

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

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

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