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: 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 : α) → β key → 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_1 : a → Type u_2} → Inhabited (Std.DHashMap.Internal.AssocList a a_1)

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

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