Documentation

Lean.Data.AssocList

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 α β

Instances For

instance Lean.instInhabitedAssocList {a✝ : Type u_1} {a✝¹ : Type u_2} :

Inhabited (AssocList a✝ a✝¹)

Equations

Lean.instInhabitedAssocList = { default := Lean.AssocList.nil }

@[reducible, inline]

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

AssocList α β

Equations

Lean.AssocList.empty = Lean.AssocList.nil

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

EmptyCollection (AssocList α β)

Equations

Lean.AssocList.instEmptyCollection = { emptyCollection := Lean.AssocList.empty }

@[reducible, inline]

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

AssocList α β

Equations

m.insertNew k v = Lean.AssocList.cons k v m

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

AssocList α β → Bool

Equations

Lean.AssocList.nil.isEmpty = true
x✝.isEmpty = false

@[specialize #[]]

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

AssocList α β → m δ

Equations

Lean.AssocList.foldlM f x✝ Lean.AssocList.nil = pure x✝
Lean.AssocList.foldlM f x✝ (Lean.AssocList.cons a b es) = do let d ← f x✝ a b Lean.AssocList.foldlM f d es

@[inline]

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

δ

Equations

Lean.AssocList.foldl f init as = (Lean.AssocList.foldlM f init as).run

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

List (α × β)

Equations

as.toList = (Lean.AssocList.foldl (fun (r : List (α × β)) (a : α) (b : β) => (a, b) :: r) [] as).reverse

@[specialize #[]]

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

AssocList α β → m PUnit

Equations

Lean.AssocList.forM f Lean.AssocList.nil = pure PUnit.unit
Lean.AssocList.forM f (Lean.AssocList.cons a b es) = do f a b Lean.AssocList.forM f es

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

AssocList α β → AssocList δ β

Equations

Lean.AssocList.mapKey f Lean.AssocList.nil = Lean.AssocList.nil
Lean.AssocList.mapKey f (Lean.AssocList.cons a b es) = Lean.AssocList.cons (f a) b (Lean.AssocList.mapKey f es)

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

AssocList α β → AssocList α δ

Equations

Lean.AssocList.mapVal f Lean.AssocList.nil = Lean.AssocList.nil
Lean.AssocList.mapVal f (Lean.AssocList.cons a b es) = Lean.AssocList.cons a (f b) (Lean.AssocList.mapVal f es)

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

AssocList α β → Option (α × β)

Equations

Lean.AssocList.findEntry? a Lean.AssocList.nil = none
Lean.AssocList.findEntry? a (Lean.AssocList.cons a_1 b es) = match a_1 == a with | true => some (a_1, b) | false => Lean.AssocList.findEntry? a es

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

AssocList α β → Option β

Equations

Lean.AssocList.find? a Lean.AssocList.nil = none
Lean.AssocList.find? a (Lean.AssocList.cons a_1 b es) = match a_1 == a with | true => some b | false => Lean.AssocList.find? a es

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

AssocList α β → Bool

Equations

Lean.AssocList.contains a Lean.AssocList.nil = false
Lean.AssocList.contains a (Lean.AssocList.cons a_1 b es) = (a_1 == a || Lean.AssocList.contains a es)

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

AssocList α β → AssocList α β

Equations

Lean.AssocList.replace a b Lean.AssocList.nil = Lean.AssocList.nil
Lean.AssocList.replace a b (Lean.AssocList.cons a_1 b_1 es) = match a_1 == a with | true => Lean.AssocList.cons a b es | false => Lean.AssocList.cons a_1 b_1 (Lean.AssocList.replace a b es)

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

AssocList α β

Equations

m.insert k v = if Lean.AssocList.contains k m = true then Lean.AssocList.replace k v m else m.insertNew k v

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

AssocList α β → AssocList α β

Equations

Lean.AssocList.erase a Lean.AssocList.nil = Lean.AssocList.nil
Lean.AssocList.erase a (Lean.AssocList.cons a_1 b es) = match a_1 == a with | true => es | false => Lean.AssocList.cons a_1 b (Lean.AssocList.erase a es)

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

AssocList α β → Bool

Equations

Lean.AssocList.any p Lean.AssocList.nil = false
Lean.AssocList.any p (Lean.AssocList.cons a b es) = (p a b || Lean.AssocList.any p es)

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

AssocList α β → Bool

Equations

Lean.AssocList.all p Lean.AssocList.nil = true
Lean.AssocList.all p (Lean.AssocList.cons a b es) = (p a b && Lean.AssocList.all p es)

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

Equations

as.forIn init f = Lean.AssocList.forIn.loop f init as

@[specialize #[]]

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

δ → AssocList α β → m δ

Equations

One or more equations did not get rendered due to their size.
Lean.AssocList.forIn.loop f x✝ Lean.AssocList.nil = pure x✝

instance Lean.AssocList.instForInProd {α : Type u} {β : Type v} {m : Type w → Type w} :

ForIn m (AssocList α β) (α × β)

Equations

Lean.AssocList.instForInProd = { forIn := fun {β_1 : Type ?u.19} [Monad m] => Lean.AssocList.forIn }

def List.toAssocList' {α : Type u} {β : Type v} :

List (α × β) → Lean.AssocList α β

Equations

[].toAssocList' = Lean.AssocList.nil
((a, b) :: es).toAssocList' = Lean.AssocList.cons a b es.toAssocList'