This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file.

Note that some functions in this file (in particular, foldrM, foldr, toList, replace, and erase) are not tail-recursive. This is not a problem because they are only used internally by HashMap, where AssocList is always small. Before making this API public, we would need to add @[csimp] lemmas for tail-recursive implementations.

File contents: Operations on associative lists

inductive Std.DHashMap.Internal.AssocList (α : Type u) (β : α → Type v) : Type (max u v)

AssocList α β is "the same as" List (α × β), but flattening the structure leads to one fewer pointer indirection (in the current code generator).

• nil {α : Type u} {β : α → Type v} : AssocList α β

  Internal implementation detail of the hash map

• cons {α : Type u} {β : α → Type v} (key : α) (value : β key) (tail : AssocList α β) : AssocList α β

  Internal implementation detail of the hash map

instance Std.DHashMap.Internal.instInhabitedAssocList {a✝ : Type u_1} {a✝¹ : a✝ → Type u_2} : Inhabited (AssocList a✝ a✝¹)

@[specialize #[]]

def Std.DHashMap.Internal.AssocList.foldlM {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → (a : α) → β a → m δ) (init : δ) : AssocList α β → m δ

Internal implementation detail of the hash map

@[inline]

def Std.DHashMap.Internal.AssocList.foldl {α : Type u} {β : α → Type v} {δ : Type w} (f : δ → (α : α) → β α → δ) (init : δ) (as : AssocList α β) : δ

Internal implementation detail of the hash map

@[specialize #[]]

def Std.DHashMap.Internal.AssocList.foldrM {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w} [Monad m] (f : (a : α) → β a → δ → m δ) (init : δ) : AssocList α β → m δ

Internal implementation detail of the hash map

@[inline]

def Std.DHashMap.Internal.AssocList.foldr {α : Type u} {β : α → Type v} {δ : Type w} (f : (a : α) → β a → δ → δ) (init : δ) (as : AssocList α β) : δ

Internal implementation detail of the hash map

@[inline]

def Std.DHashMap.Internal.AssocList.forM {α : Type u} {β : α → Type v} {m : Type w → Type w} [Monad m] (f : (a : α) → β a → m PUnit) (as : AssocList α β) : m PUnit

Internal implementation detail of the hash map

@[inline]

def Std.DHashMap.Internal.AssocList.forInStep {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w} [Monad m] (as : AssocList α β) (init : δ) (f : (a : α) → β a → δ → m (ForInStep δ)) : m (ForInStep δ)

Internal implementation detail of the hash map

@[specialize #[]]

def Std.DHashMap.Internal.AssocList.forInStep.go {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w} [Monad m] (f : (a : α) → β a → δ → m (ForInStep δ)) : AssocList α β → δ → m (ForInStep δ)

def Std.DHashMap.Internal.AssocList.toList {α : Type u} {β : α → Type v} : AssocList α β → List ((a : α) × β a)

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.length {α : Type u} {β : α → Type v} (l : AssocList α β) : Nat

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.get? {α : Type u} {β : Type v} [BEq α] (a : α) : (AssocList α fun (x : α) => β) → Option β

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.getCast? {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (a : α) : AssocList α β → Option (β a)

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.contains {α : Type u} {β : α → Type v} [BEq α] (a : α) : AssocList α β → Bool

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.get {α : Type u} {β : Type v} [BEq α] (a : α) (l : AssocList α fun (x : α) => β) : contains a l = true → β

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.getCast {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (a : α) (l : AssocList α β) : contains a l = true → β a

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.getKey {α : Type u} {β : α → Type v} [BEq α] (a : α) (l : AssocList α β) : contains a l = true → α

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.getCast! {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (a : α) [Inhabited (β a)] : AssocList α β → β a

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.getKey? {α : Type u} {β : α → Type v} [BEq α] (a : α) : AssocList α β → Option α

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.get! {α : Type u} {β : Type v} [BEq α] [Inhabited β] (a : α) : (AssocList α fun (x : α) => β) → β

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.getKey! {α : Type u} {β : α → Type v} [BEq α] [Inhabited α] (a : α) : AssocList α β → α

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.getCastD {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (a : α) (fallback : β a) : AssocList α β → β a

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.getD {α : Type u} {β : Type v} [BEq α] (a : α) (fallback : β) : (AssocList α fun (x : α) => β) → β

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.getKeyD {α : Type u} {β : α → Type v} [BEq α] (a fallback : α) : AssocList α β → α

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.replace {α : Type u} {β : α → Type v} [BEq α] (a : α) (b : β a) : AssocList α β → AssocList α β

Internal implementation detail of the hash map

def Std.DHashMap.Internal.AssocList.erase {α : Type u} {β : α → Type v} [BEq α] (a : α) : AssocList α β → AssocList α β

Internal implementation detail of the hash map

@[specialize #[]]

def Std.DHashMap.Internal.AssocList.modify {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (a : α) (f : β a → β a) : AssocList α β → AssocList α β

Internal implementation detail of the hash map

@[specialize #[]]

def Std.DHashMap.Internal.AssocList.alter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (a : α) (f : Option (β a) → Option (β a)) : AssocList α β → AssocList α β

Internal implementation detail of the hash map

@[specialize #[]]

def Std.DHashMap.Internal.AssocList.Const.modify {α : Type u} [BEq α] {β : Type v} (a : α) (f : β → β) : (AssocList α fun (x : α) => β) → AssocList α fun (x : α) => β

Internal implementation detail of the hash map

@[specialize #[]]

def Std.DHashMap.Internal.AssocList.Const.alter {α : Type u} [BEq α] {β : Type v} (a : α) (f : Option β → Option β) : (AssocList α fun (x : α) => β) → AssocList α fun (x : α) => β

Internal implementation detail of the hash map

@[inline]

def Std.DHashMap.Internal.AssocList.filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → Option (γ a)) : AssocList α β → AssocList α γ

Internal implementation detail of the hash map

@[specialize #[]]

def Std.DHashMap.Internal.AssocList.filterMap.go {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → Option (γ a)) (acc : AssocList α γ) : AssocList α β → AssocList α γ

@[inline]

def Std.DHashMap.Internal.AssocList.map {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → γ a) : AssocList α β → AssocList α γ

Internal implementation detail of the hash map

@[specialize #[]]

def Std.DHashMap.Internal.AssocList.map.go {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → γ a) (acc : AssocList α γ) : AssocList α β → AssocList α γ

@[inline]

def Std.DHashMap.Internal.AssocList.filter {α : Type u} {β : α → Type v} (f : (a : α) → β a → Bool) : AssocList α β → AssocList α β

Internal implementation detail of the hash map

@[specialize #[]]

def Std.DHashMap.Internal.AssocList.filter.go {α : Type u} {β : α → Type v} (f : (a : α) → β a → Bool) (acc : AssocList α β) : AssocList α β → AssocList α β