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

source
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

Instances For

source
def Std.DHashMap.Internal.instInhabitedAssocList.default {a✝ : Type u_1} {a✝¹ : a✝ → Type u_2} :
AssocList a✝ a✝¹
Equations

- Std.DHashMap.Internal.instInhabitedAssocList.default = Std.DHashMap.Internal.AssocList.nil

Instances For

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

- Std.DHashMap.Internal.instInhabitedAssocList = { default := Std.DHashMap.Internal.instInhabitedAssocList.default }

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

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

Instances For

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

Internal implementation detail of the hash map

Equations

- Std.DHashMap.Internal.AssocList.foldl f init as = (Std.DHashMap.Internal.AssocList.foldlM (fun (x1 : δ) (x2 : α) (x3 : β x2) => pure (f x1 x2 x3)) init as).run

Instances For

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

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

Instances For

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

Equations

- Std.DHashMap.Internal.AssocList.foldr f init as = (Std.DHashMap.Internal.AssocList.foldrM (fun (x1 : α) (x2 : β x1) (x3 : δ) => pure (f x1 x2 x3)) init as).run

Instances For

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

Equations

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

Instances For

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

Equations

- as.forInStep init f = Std.DHashMap.Internal.AssocList.forInStep.go✝ f as init

Instances For

source
def Std.DHashMap.Internal.AssocList.toList {α : Type u} {β : α → Type v} :
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

Instances For

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

Internal implementation detail of the hash map

Equations

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

Instances For

source
def Std.DHashMap.Internal.AssocList.get? {α : Type u} {β : Type v} [BEq α] (a : α) :
(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

Instances For

source
def Std.DHashMap.Internal.AssocList.getCast? {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (a : α) :
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

Instances For

source
def Std.DHashMap.Internal.AssocList.contains {α : Type u} {β : α → Type v} [BEq α] (a : α) :
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)

Instances For

source
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

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 ⋯

Instances For

source
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

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 ⋯

Instances For

source
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

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 ⋯

Instances For

source
def Std.DHashMap.Internal.AssocList.getCast! {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (a : α) [Inhabited (β a)] :
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

Instances For

source
def Std.DHashMap.Internal.AssocList.getKey? {α : Type u} {β : α → Type v} [BEq α] (a : α) :
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

Instances For

source
def Std.DHashMap.Internal.AssocList.get! {α : Type u} {β : Type v} [BEq α] [Inhabited β] (a : α) :
(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

Instances For

source
def Std.DHashMap.Internal.AssocList.getKey! {α : Type u} {β : α → Type v} [BEq α] [Inhabited α] (a : α) :
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

Instances For

source
def Std.DHashMap.Internal.AssocList.getCastD {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (a : α) (fallback : β a) :
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

Instances For

source
def Std.DHashMap.Internal.AssocList.getD {α : Type u} {β : Type v} [BEq α] (a : α) (fallback : β) :
(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

Instances For

source
def Std.DHashMap.Internal.AssocList.getKeyD {α : Type u} {β : α → Type v} [BEq α] (a fallback : α) :
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

Instances For

source
def Std.DHashMap.Internal.AssocList.replace {α : Type u} {β : α → Type v} [BEq α] (a : α) (b : β a) :
AssocList α β → 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

Instances For

source
def Std.DHashMap.Internal.AssocList.erase {α : Type u} {β : α → Type v} [BEq α] (a : α) :
AssocList α β → 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

Instances For

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

Equations

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

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Equations

- One or more equations did not get rendered due to their size.
- Std.DHashMap.Internal.AssocList.Const.modify a f Std.DHashMap.Internal.AssocList.nil = Std.DHashMap.Internal.AssocList.nil

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Equations

- Std.DHashMap.Internal.AssocList.filterMap f = Std.DHashMap.Internal.AssocList.filterMap.go✝ f Std.DHashMap.Internal.AssocList.nil

Instances For

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

Equations

- Std.DHashMap.Internal.AssocList.map f = Std.DHashMap.Internal.AssocList.map.go✝ f Std.DHashMap.Internal.AssocList.nil

Instances For

source
@[inline]
def Std.DHashMap.Internal.AssocList.filter {α : Type u} {β : α → Type v} (f : (a : α) → β a → Bool) :
AssocList α β → 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

Instances For