inductive Lean.AssocList (α : Type u) (β : Type v) : Type (max u v)

List-like type to avoid extra level of indirection

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

def Lean.instInhabitedAssocList.default {a✝ : Type u_1} {a✝¹ : Type u_2} : AssocList a✝ a✝¹

instance Lean.instInhabitedAssocList {a✝ : Type u_1} {a✝¹ : Type u_2} : Inhabited (AssocList a✝ a✝¹)

@[reducible, inline]

abbrev Lean.AssocList.empty {α : Type u} {β : Type v} : AssocList α β

instance Lean.AssocList.instEmptyCollection {α : Type u} {β : Type v} : EmptyCollection (AssocList α β)

@[reducible, inline]

abbrev Lean.AssocList.insertNew {α : Type u} {β : Type v} (m : AssocList α β) (k : α) (v : β) : AssocList α β

def Lean.AssocList.isEmpty {α : Type u} {β : Type v} : AssocList α β → Bool

@[specialize #[]]

def Lean.AssocList.foldlM {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] (f : δ → α → β → m δ) (init : δ) : AssocList α β → m δ

@[inline]

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

def Lean.AssocList.toList {α : Type u} {β : Type v} (as : AssocList α β) : List (α × β)

@[specialize #[]]

def Lean.AssocList.forM {α : Type u} {β : Type v} {m : Type w → Type w'} [Monad m] (f : α → β → m PUnit) : AssocList α β → m PUnit

def Lean.AssocList.mapKey {α : Type u} {β : Type v} {δ : Type w} (f : α → δ) : AssocList α β → AssocList δ β

def Lean.AssocList.mapVal {α : Type u} {β : Type v} {δ : Type w} (f : β → δ) : AssocList α β → AssocList α δ

def Lean.AssocList.findEntry? {α : Type u} {β : Type v} [BEq α] (a : α) : AssocList α β → Option (α × β)

def Lean.AssocList.find? {α : Type u} {β : Type v} [BEq α] (a : α) : AssocList α β → Option β

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

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

def Lean.AssocList.insert {α : Type u} {β : Type v} [BEq α] (m : AssocList α β) (k : α) (v : β) : AssocList α β

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

def Lean.AssocList.any {α : Type u} {β : Type v} (p : α → β → Bool) : AssocList α β → Bool

def Lean.AssocList.all {α : Type u} {β : Type v} (p : α → β → Bool) : AssocList α β → Bool

@[inline]

def Lean.AssocList.forIn {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] (as : AssocList α β) (init : δ) (f : α × β → δ → m (ForInStep δ)) : m δ

instance Lean.AssocList.instForInProdOfMonad {α : Type u} {β : Type v} {m : Type w → Type w'} [Monad m] : ForIn m (AssocList α β) (α × β)

def List.toAssocList' {α : Type u} {β : Type v} : List (α × β) → Lean.AssocList α β