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.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.get?_eq
{α : Type u}
{β : Type v}
[BEq α]
{l : AssocList α fun (x : α) => β}
{a : α}
:
get? a l = 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 = List.getValueCast? a l.toList
@[simp]
theorem
Std.DHashMap.Internal.AssocList.contains_eq
{α : Type u}
{β : α → Type v}
[BEq α]
{l : AssocList α β}
{a : α}
:
contains a l = List.containsKey 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 = 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 = 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.get!_eq
{α : Type u}
{β : Type v}
[BEq α]
[Inhabited β]
{l : AssocList α fun (x : α) => β}
{a : α}
:
get! a l = List.getValue! a l.toList
@[simp]
theorem
Std.DHashMap.Internal.AssocList.getKey?_eq
{α : Type u}
{β : α → Type v}
[BEq α]
{l : AssocList α β}
{a : α}
:
getKey? a l = 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 = 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 = 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 = 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 = 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_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)