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} : Std.DHashMap.Internal.AssocList α β

  Internal implementation detail of the hash map

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

  Internal implementation detail of the hash map

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

Equations

• Std.DHashMap.Internal.instInhabitedAssocList = { default := Std.DHashMap.Internal.AssocList.nil }

@[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 : δ) : Std.DHashMap.Internal.AssocList α β → m δ

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.foldlM f x✝ Std.DHashMap.Internal.AssocList.nil = pure x✝
• Std.DHashMap.Internal.AssocList.foldlM f x✝ (Std.DHashMap.Internal.AssocList.cons a b es) = do let d ← f x✝ a b Std.DHashMap.Internal.AssocList.foldlM f d es

@[inline]

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.foldl f init as = (Std.DHashMap.Internal.AssocList.foldlM f init as).run

@[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 : δ) : Std.DHashMap.Internal.AssocList α β → m δ

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.foldrM f x✝ Std.DHashMap.Internal.AssocList.nil = pure x✝
• Std.DHashMap.Internal.AssocList.foldrM f x✝ (Std.DHashMap.Internal.AssocList.cons a b es) = do let d ← Std.DHashMap.Internal.AssocList.foldrM f x✝ es f a b d

@[inline]

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.foldr f init as = (Std.DHashMap.Internal.AssocList.foldrM f init as).run

@[inline]

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.forM f as = Std.DHashMap.Internal.AssocList.foldlM (fun (x : PUnit) => f) PUnit.unit as

@[inline]

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

Internal implementation detail of the hash map

Equations

• as.forInStep init f = Std.DHashMap.Internal.AssocList.forInStep.go f as init

@[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 δ)) : Std.DHashMap.Internal.AssocList α β → δ → m (ForInStep δ)

Equations

• One or more equations did not get rendered due to their size.
• Std.DHashMap.Internal.AssocList.forInStep.go f Std.DHashMap.Internal.AssocList.nil x✝ = pure (ForInStep.yield x✝)

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.nil.toList = []
• (Std.DHashMap.Internal.AssocList.cons a b es).toList = ⟨a, b⟩ :: es.toList

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

Internal implementation detail of the hash map

Equations

• l.length = Std.DHashMap.Internal.AssocList.foldl (fun (n : Nat) (x : α) (x : β x) => n + 1) 0 l

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.get? a Std.DHashMap.Internal.AssocList.nil = none
• Std.DHashMap.Internal.AssocList.get? a (Std.DHashMap.Internal.AssocList.cons k v es) = bif k == a then some v else Std.DHashMap.Internal.AssocList.get? a es

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.getCast? a Std.DHashMap.Internal.AssocList.nil = none
• Std.DHashMap.Internal.AssocList.getCast? a (Std.DHashMap.Internal.AssocList.cons a_1 b es) = if h : (a_1 == a) = true then some (cast ⋯ b) else Std.DHashMap.Internal.AssocList.getCast? a es

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.contains a Std.DHashMap.Internal.AssocList.nil = false
• Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons a_1 b es) = (a_1 == a || Std.DHashMap.Internal.AssocList.contains a es)

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.get a (Std.DHashMap.Internal.AssocList.cons k v es) h = if hka : (k == a) = true then v else Std.DHashMap.Internal.AssocList.get a es ⋯

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.getCast a (Std.DHashMap.Internal.AssocList.cons k v es) h = if hka : (k == a) = true then cast ⋯ v else Std.DHashMap.Internal.AssocList.getCast a es ⋯

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.getKey a (Std.DHashMap.Internal.AssocList.cons k v es) h = if hka : (k == a) = true then k else Std.DHashMap.Internal.AssocList.getKey a es ⋯

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

Internal implementation detail of the hash map

Equations

• One or more equations did not get rendered due to their size.
• Std.DHashMap.Internal.AssocList.getCast! a (Std.DHashMap.Internal.AssocList.cons a_1 b es) = if h : (a_1 == a) = true then cast ⋯ b else Std.DHashMap.Internal.AssocList.getCast! a es

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.getKey? a Std.DHashMap.Internal.AssocList.nil = none
• Std.DHashMap.Internal.AssocList.getKey? a (Std.DHashMap.Internal.AssocList.cons a_1 b es) = if (a_1 == a) = true then some a_1 else Std.DHashMap.Internal.AssocList.getKey? a es

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

Internal implementation detail of the hash map

Equations

• One or more equations did not get rendered due to their size.
• Std.DHashMap.Internal.AssocList.get! a (Std.DHashMap.Internal.AssocList.cons k v es) = bif k == a then v else Std.DHashMap.Internal.AssocList.get! a es

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

Internal implementation detail of the hash map

Equations

• One or more equations did not get rendered due to their size.
• Std.DHashMap.Internal.AssocList.getKey! a (Std.DHashMap.Internal.AssocList.cons a_1 b es) = if (a_1 == a) = true then a_1 else Std.DHashMap.Internal.AssocList.getKey! a es

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

Internal implementation detail of the hash map

Equations

• One or more equations did not get rendered due to their size.
• Std.DHashMap.Internal.AssocList.getCastD a fallback Std.DHashMap.Internal.AssocList.nil = fallback

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.getD a fallback Std.DHashMap.Internal.AssocList.nil = fallback
• Std.DHashMap.Internal.AssocList.getD a fallback (Std.DHashMap.Internal.AssocList.cons k v es) = bif k == a then v else Std.DHashMap.Internal.AssocList.getD a fallback es

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.getKeyD a fallback Std.DHashMap.Internal.AssocList.nil = fallback
• Std.DHashMap.Internal.AssocList.getKeyD a fallback (Std.DHashMap.Internal.AssocList.cons a_1 b es) = if (a_1 == a) = true then a_1 else Std.DHashMap.Internal.AssocList.getKeyD a fallback es

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

Internal implementation detail of the hash map

Equations

• One or more equations did not get rendered due to their size.
• Std.DHashMap.Internal.AssocList.replace a b Std.DHashMap.Internal.AssocList.nil = Std.DHashMap.Internal.AssocList.nil

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

Internal implementation detail of the hash map

Equations

• One or more equations did not get rendered due to their size.
• Std.DHashMap.Internal.AssocList.erase a Std.DHashMap.Internal.AssocList.nil = Std.DHashMap.Internal.AssocList.nil

@[inline]

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.filterMap f = Std.DHashMap.Internal.AssocList.filterMap.go f Std.DHashMap.Internal.AssocList.nil

@[specialize #[]]

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

Equations

• One or more equations did not get rendered due to their size.
• Std.DHashMap.Internal.AssocList.filterMap.go f acc Std.DHashMap.Internal.AssocList.nil = acc

@[inline]

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.map f = Std.DHashMap.Internal.AssocList.map.go f Std.DHashMap.Internal.AssocList.nil

@[specialize #[]]

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

Equations

• Std.DHashMap.Internal.AssocList.map.go f acc Std.DHashMap.Internal.AssocList.nil = acc
• Std.DHashMap.Internal.AssocList.map.go f acc (Std.DHashMap.Internal.AssocList.cons a b es) = Std.DHashMap.Internal.AssocList.map.go f (Std.DHashMap.Internal.AssocList.cons a (f a b) acc) es

@[inline]

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

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.AssocList.filter f = Std.DHashMap.Internal.AssocList.filter.go f Std.DHashMap.Internal.AssocList.nil

@[specialize #[]]

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

Equations

• One or more equations did not get rendered due to their size.
• Std.DHashMap.Internal.AssocList.filter.go f acc Std.DHashMap.Internal.AssocList.nil = acc