Documentation

Std.Data.AssocList

inductive Std.AssocList (α : Type u) (β : Type v) :

Type (max u v)

nil: {α : Type u} → {β : Type v} → Std.AssocList α β
cons: {α : Type u} → {β : Type v} → α → β → Std.AssocList α β → Std.AssocList α β

instance Std.instInhabitedAssocList :

{a : Type u_1} → {a_1 : Type u_2} → Inhabited (Std.AssocList a a_1)

Equations

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

@[inline]

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

Std.AssocList α β

Equations

Std.AssocList.empty = Std.AssocList.nil

instance Std.AssocList.instEmptyCollectionAssocList {α : Type u} {β : Type v} :

EmptyCollection (Std.AssocList α β)

Equations

Std.AssocList.instEmptyCollectionAssocList = { emptyCollection := Std.AssocList.empty }

@[inline]

abbrev Std.AssocList.insert {α : Type u} {β : Type v} (m : Std.AssocList α β) (k : α) (v : β) :

Std.AssocList α β

Equations

Std.AssocList.insert m k v = Std.AssocList.cons k v m

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

Std.AssocList α β → Bool

Equations

Std.AssocList.isEmpty x = match x with | Std.AssocList.nil => true | x => false

@[specialize]

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

Std.AssocList α β → m δ

Equations

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

@[inline]

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

δ

Equations

Std.AssocList.foldl f init as = Id.run (Std.AssocList.foldlM f init as)

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

List (α × β)

Equations

Std.AssocList.toList as = List.reverse (Std.AssocList.foldl (fun r a b => (a, b) :: r) [] as)

@[specialize]

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

Std.AssocList α β → m PUnit

Equations

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

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

Std.AssocList α β → Std.AssocList δ β

Equations

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

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

Std.AssocList α β → Std.AssocList α δ

Equations

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

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

Std.AssocList α β → Option (α × β)

Equations

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

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

Std.AssocList α β → Option β

Equations

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

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

Std.AssocList α β → Bool

Equations

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

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

Std.AssocList α β → Std.AssocList α β

Equations

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

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

Std.AssocList α β → Std.AssocList α β

Equations

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

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

Std.AssocList α β → Bool

Equations

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

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

Std.AssocList α β → Bool

Equations

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

@[inline]

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

m δ

Equations

Std.AssocList.forIn as init f = (fun loop => loop init as) (Std.AssocList.forIn.loop f)

@[specialize]

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

δ → Std.AssocList α β → m δ

Equations

Std.AssocList.forIn.loop f x Std.AssocList.nil = pure x
Std.AssocList.forIn.loop f x (Std.AssocList.cons a b es) = do let a ← f (a, b) x match a with | ForInStep.done d => pure d | ForInStep.yield d => Std.AssocList.forIn.loop f d es

instance Std.AssocList.instForInAssocListProd {α : Type u} {β : Type v} {m : Type w → Type w} :

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

Equations

Std.AssocList.instForInAssocListProd = { forIn := fun {β} [Monad m] => Std.AssocList.forIn }

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

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

Equations

List.toAssocList [] = Std.AssocList.nil
List.toAssocList ((a, b) :: es) = Std.AssocList.cons a b (List.toAssocList es)