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}
:
Std.DHashMap.Internal.AssocList.nil.toList = []
@[simp]
theorem
Std.DHashMap.Internal.AssocList.toList_cons
{α : Type u}
{β : α → Type v}
{l : Std.DHashMap.Internal.AssocList α β}
{a : α}
{b : β a}
:
(Std.DHashMap.Internal.AssocList.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 : Std.DHashMap.Internal.AssocList α β}
:
Std.DHashMap.Internal.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 : Std.DHashMap.Internal.AssocList α β}
:
l.length = l.toList.length
@[simp]
theorem
Std.DHashMap.Internal.AssocList.get?_eq
{α : Type u}
{β : Type v}
[BEq α]
{l : Std.DHashMap.Internal.AssocList α fun (x : α) => β}
{a : α}
:
@[simp]
theorem
Std.DHashMap.Internal.AssocList.getCast?_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[LawfulBEq α]
{l : Std.DHashMap.Internal.AssocList α β}
{a : α}
:
@[simp]
theorem
Std.DHashMap.Internal.AssocList.contains_eq
{α : Type u}
{β : α → Type v}
[BEq α]
{l : Std.DHashMap.Internal.AssocList α β}
{a : α}
:
@[simp]
theorem
Std.DHashMap.Internal.AssocList.getCast_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[LawfulBEq α]
{l : Std.DHashMap.Internal.AssocList α β}
{a : α}
{h : Std.DHashMap.Internal.AssocList.contains a l = true}
:
Std.DHashMap.Internal.AssocList.getCast a l h = Std.DHashMap.Internal.List.getValueCast a l.toList ⋯
@[simp]
theorem
Std.DHashMap.Internal.AssocList.get_eq
{α : Type u}
{β : Type v}
[BEq α]
{l : Std.DHashMap.Internal.AssocList α fun (x : α) => β}
{a : α}
{h : Std.DHashMap.Internal.AssocList.contains a l = true}
:
Std.DHashMap.Internal.AssocList.get a l h = Std.DHashMap.Internal.List.getValue a l.toList ⋯
@[simp]
theorem
Std.DHashMap.Internal.AssocList.getCastD_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[LawfulBEq α]
{l : Std.DHashMap.Internal.AssocList α β}
{a : α}
{fallback : β a}
:
Std.DHashMap.Internal.AssocList.getCastD a fallback l = Std.DHashMap.Internal.List.getValueCastD a l.toList fallback
@[simp]
theorem
Std.DHashMap.Internal.AssocList.getD_eq
{α : Type u}
{β : Type v}
[BEq α]
{l : Std.DHashMap.Internal.AssocList α fun (x : α) => β}
{a : α}
{fallback : β}
:
Std.DHashMap.Internal.AssocList.getD a fallback l = Std.DHashMap.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 : Std.DHashMap.Internal.AssocList α β}
{a : α}
[Inhabited (β a)]
:
@[simp]
theorem
Std.DHashMap.Internal.AssocList.get!_eq
{α : Type u}
{β : Type v}
[BEq α]
[Inhabited β]
{l : Std.DHashMap.Internal.AssocList α fun (x : α) => β}
{a : α}
:
@[simp]
theorem
Std.DHashMap.Internal.AssocList.getKey?_eq
{α : Type u}
{β : α → Type v}
[BEq α]
{l : Std.DHashMap.Internal.AssocList α β}
{a : α}
:
@[simp]
theorem
Std.DHashMap.Internal.AssocList.getKey_eq
{α : Type u}
{β : α → Type v}
[BEq α]
{l : Std.DHashMap.Internal.AssocList α β}
{a : α}
{h : Std.DHashMap.Internal.AssocList.contains a l = true}
:
Std.DHashMap.Internal.AssocList.getKey a l h = Std.DHashMap.Internal.List.getKey a l.toList ⋯
@[simp]
theorem
Std.DHashMap.Internal.AssocList.getKeyD_eq
{α : Type u}
{β : α → Type v}
[BEq α]
{l : Std.DHashMap.Internal.AssocList α β}
{a fallback : α}
:
Std.DHashMap.Internal.AssocList.getKeyD a fallback l = Std.DHashMap.Internal.List.getKeyD a l.toList fallback
@[simp]
theorem
Std.DHashMap.Internal.AssocList.getKey!_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Inhabited α]
{l : Std.DHashMap.Internal.AssocList α β}
{a : α}
:
@[simp]
theorem
Std.DHashMap.Internal.AssocList.toList_replace
{α : Type u}
{β : α → Type v}
[BEq α]
{l : Std.DHashMap.Internal.AssocList α β}
{a : α}
{b : β a}
:
(Std.DHashMap.Internal.AssocList.replace a b l).toList = Std.DHashMap.Internal.List.replaceEntry a b l.toList
@[simp]
theorem
Std.DHashMap.Internal.AssocList.toList_erase
{α : Type u}
{β : α → Type v}
[BEq α]
{l : Std.DHashMap.Internal.AssocList α β}
{a : α}
:
(Std.DHashMap.Internal.AssocList.erase a l).toList = Std.DHashMap.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 : Std.DHashMap.Internal.AssocList α β}
:
(Std.DHashMap.Internal.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 : Std.DHashMap.Internal.AssocList α β}
:
(Std.DHashMap.Internal.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 : Std.DHashMap.Internal.AssocList α β}
:
(Std.DHashMap.Internal.AssocList.filter f l).toList.Perm
(List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l.toList)
theorem
Std.DHashMap.Internal.AssocList.foldl_apply
{α : Type u}
{β : α → Type v}
{δ : Type w}
{l : Std.DHashMap.Internal.AssocList α β}
{acc : List δ}
(f : (a : α) → β a → δ)
: