# Documentation

## Batteries.Data.AssocList

inductive Batteries.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). It is mainly intended as a component of HashMap, but it can also be used as a plain key-value map.

• nil: {α : Type u} → {β : Type v} →

An empty list

• cons: {α : Type u} → {β : Type v} → αβ

Add a key, value pair to the list

Instances For
instance Batteries.instInhabitedAssocList :
{a : Type u_1} → {a_1 : Type u_2} → Inhabited (Batteries.AssocList a a_1)
Equations
• Batteries.instInhabitedAssocList = { default := Batteries.AssocList.nil }
def Batteries.AssocList.toList {α : Type u_1} {β : Type u_2} :
List (α × β)

O(n). Convert an AssocList α β into the equivalent List (α × β). This is used to give specifications for all the AssocList functions in terms of corresponding list functions.

Equations
Instances For
instance Batteries.AssocList.instEmptyCollection {α : Type u_1} {β : Type u_2} :
Equations
• Batteries.AssocList.instEmptyCollection = { emptyCollection := Batteries.AssocList.nil }
@[simp]
theorem Batteries.AssocList.empty_eq {α : Type u_1} {β : Type u_2} :
= Batteries.AssocList.nil
def Batteries.AssocList.isEmpty {α : Type u_1} {β : Type u_2} :

O(1). Is the list empty?

Equations
• x.isEmpty = match x with | Batteries.AssocList.nil => true | x => false
Instances For
@[simp]
theorem Batteries.AssocList.isEmpty_eq {α : Type u_1} {β : Type u_2} (l : ) :
l.isEmpty = l.toList.isEmpty
def Batteries.AssocList.length {α : Type u_1} {β : Type u_2} (L : ) :

The number of entries in an AssocList.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.length_nil {α : Type u_1} {β : Type u_2} :
Batteries.AssocList.nil.length = 0
@[simp]
theorem Batteries.AssocList.length_cons :
∀ {α : Type u_1} {a : α} {β : Type u_2} {b : β} {t : }, .length = t.length + 1
theorem Batteries.AssocList.length_toList {α : Type u_1} {β : Type u_2} (l : ) :
l.toList.length = l.length
@[specialize #[]]
def Batteries.AssocList.foldlM {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [] (f : δαβm δ) (init : δ) :
m δ

O(n). Fold a monadic function over the list, from head to tail.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.foldlM_eq {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [] (f : δαβm δ) (init : δ) (l : ) :
= List.foldlM (fun (d : δ) (x : α × β) => match x with | (a, b) => f d a b) init l.toList
@[inline]
def Batteries.AssocList.foldl {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δαβδ) (init : δ) (as : ) :
δ

O(n). Fold a function over the list, from head to tail.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.foldl_eq {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δαβδ) (init : δ) (l : ) :
= List.foldl (fun (d : δ) (x : α × β) => match x with | (a, b) => f d a b) init l.toList
def Batteries.AssocList.toListTR {α : Type u_1} {β : Type u_2} (as : ) :
List (α × β)

Optimized version of toList.

Equations
Instances For
@[specialize #[]]
def Batteries.AssocList.forM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [] (f : αβ) :

O(n). Run monadic function f on all elements in the list, from head to tail.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.forM_eq {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [] (f : αβ) (l : ) :
= l.toList.forM fun (x : α × β) => match x with | (a, b) => f a b
def Batteries.AssocList.mapKey {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : αδ) :

O(n). Map a function f over the keys of the list.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.toList_mapKey {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : αδ) (l : ) :
.toList = List.map (fun (x : α × β) => match x with | (a, b) => (f a, b)) l.toList
@[simp]
theorem Batteries.AssocList.length_mapKey :
∀ {α : Type u_1} {α_1 : Type u_2} {f : αα_1} {β : Type u_3} {l : }, .length = l.length
def Batteries.AssocList.mapVal {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : αβδ) :

O(n). Map a function f over the values of the list.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.toList_mapVal {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : αβδ) (l : ) :
.toList = List.map (fun (x : α × β) => match x with | (a, b) => (a, f a b)) l.toList
@[simp]
theorem Batteries.AssocList.length_mapVal :
∀ {α : Type u_1} {β : Type u_2} {β_1 : Type u_3} {f : αββ_1} {l : }, .length = l.length
@[specialize #[]]
def Batteries.AssocList.findEntryP? {α : Type u_1} {β : Type u_2} (p : αβBool) :
Option (α × β)

O(n). Returns the first entry in the list whose entry satisfies p.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.findEntryP?_eq {α : Type u_1} {β : Type u_2} (p : αβBool) (l : ) :
= List.find? (fun (x : α × β) => match x with | (a, b) => p a b) l.toList
@[inline]
def Batteries.AssocList.findEntry? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : ) :
Option (α × β)

O(n). Returns the first entry in the list whose key is equal to a.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.findEntry?_eq {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : ) :
= List.find? (fun (x : α × β) => x.fst == a) l.toList
def Batteries.AssocList.find? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) :

O(n). Returns the first value in the list whose key is equal to a.

Equations
Instances For
theorem Batteries.AssocList.find?_eq_findEntry? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : ) :
= Option.map (fun (x : α × β) => x.snd)
@[simp]
theorem Batteries.AssocList.find?_eq {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : ) :
= Option.map (fun (x : α × β) => x.snd) (List.find? (fun (x : α × β) => x.fst == a) l.toList)
@[specialize #[]]
def Batteries.AssocList.any {α : Type u_1} {β : Type u_2} (p : αβBool) :

O(n). Returns true if any entry in the list satisfies p.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.any_eq {α : Type u_1} {β : Type u_2} (p : αβBool) (l : ) :
= l.toList.any fun (x : α × β) => match x with | (a, b) => p a b
@[specialize #[]]
def Batteries.AssocList.all {α : Type u_1} {β : Type u_2} (p : αβBool) :

O(n). Returns true if every entry in the list satisfies p.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.all_eq {α : Type u_1} {β : Type u_2} (p : αβBool) (l : ) :
= l.toList.all fun (x : α × β) => match x with | (a, b) => p a b
def Batteries.AssocList.All {α : Type u_1} {β : Type u_2} (p : αβProp) (l : ) :

Returns true if every entry in the list satisfies p.

Equations
• = ∀ (a : α × β), a l.toListp a.fst a.snd
Instances For
@[inline]
def Batteries.AssocList.contains {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : ) :

O(n). Returns true if there is an element in the list whose key is equal to a.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.contains_eq {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : ) :
= l.toList.any fun (x : α × β) => x.fst == a
def Batteries.AssocList.replace {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (b : β) :

O(n). Replace the first entry in the list with key equal to a to have key a and value b.

Equations
• One or more equations did not get rendered due to their size.
• Batteries.AssocList.replace a b Batteries.AssocList.nil = Batteries.AssocList.nil
Instances For
@[simp]
theorem Batteries.AssocList.toList_replace {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (b : β) (l : ) :
.toList = List.replaceF (fun (x : α × β) => bif x.fst == a then some (a, b) else none) l.toList
@[simp]
theorem Batteries.AssocList.length_replace {α : Type u_1} :
∀ {β : Type u_2} {b : β} {l : } [inst : BEq α] {a : α}, .length = l.length
@[specialize #[]]
def Batteries.AssocList.eraseP {α : Type u_1} {β : Type u_2} (p : αβBool) :

O(n). Remove the first entry in the list with key equal to a.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.toList_eraseP {α : Type u_1} {β : Type u_2} (p : αβBool) (l : ) :
.toList = List.eraseP (fun (x : α × β) => match x with | (a, b) => p a b) l.toList
@[inline]
def Batteries.AssocList.erase {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : ) :

O(n). Remove the first entry in the list with key equal to a.

Equations
Instances For
@[simp]
theorem Batteries.AssocList.toList_erase {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : ) :
.toList = List.eraseP (fun (x : α × β) => x.fst == a) l.toList
def Batteries.AssocList.modify {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (f : αββ) :

O(n). Replace the first entry a', b in the list with key equal to a to have key a and value f a' b.

Equations
• One or more equations did not get rendered due to their size.
• Batteries.AssocList.modify a f Batteries.AssocList.nil = Batteries.AssocList.nil
Instances For
@[simp]
theorem Batteries.AssocList.toList_modify {α : Type u_1} {β : Type u_2} {f : αββ} [BEq α] (a : α) (l : ) :
.toList = List.replaceF (fun (x : α × β) => match x with | (k, v) => bif k == a then some (a, f k v) else none) l.toList
@[simp]
theorem Batteries.AssocList.length_modify {α : Type u_1} :
∀ {β : Type u_2} {f : αββ} {l : } [inst : BEq α] {a : α}, .length = l.length
@[specialize #[]]
def Batteries.AssocList.forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [] (as : ) (init : δ) (f : α × βδm (ForInStep δ)) :
m δ

The implementation of ForIn, which enables for (k, v) in aList do ... notation.

Equations
• Batteries.AssocList.nil.forIn init f = pure init
• (Batteries.AssocList.cons a b es).forIn init f = do let __do_liftf (a, b) init match __do_lift with | => pure d | => es.forIn d f
Instances For
instance Batteries.AssocList.instForInProd {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} :
ForIn m (α × β)
Equations
• Batteries.AssocList.instForInProd = { forIn := fun {β_1 : Type u_1} [] => Batteries.AssocList.forIn }
@[simp]
theorem Batteries.AssocList.forIn_eq {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [] (l : ) (init : δ) (f : α × βδm (ForInStep δ)) :
forIn l init f = forIn l.toList init f
def Batteries.AssocList.pop? {α : Type u_1} {β : Type u_2} :
Option ((α × β) × )

Split the list into head and tail, if possible.

Equations
• x.pop? = match x with | Batteries.AssocList.nil => none | => some ((a, b), l)
Instances For
instance Batteries.AssocList.instToStream {α : Type u_1} {β : Type u_2} :
Equations
• Batteries.AssocList.instToStream = { toStream := fun (x : ) => x }
instance Batteries.AssocList.instStreamProd {α : Type u_1} {β : Type u_2} :
Stream (α × β)
Equations
• Batteries.AssocList.instStreamProd = { next? := Batteries.AssocList.pop? }
def List.toAssocList {α : Type u_1} {β : Type u_2} :
List (α × β)

Converts a list into an AssocList. This is the inverse function to AssocList.toList.

Equations
Instances For
@[simp]
theorem List.toList_toAssocList {α : Type u_1} {β : Type u_2} (l : List (α × β)) :
l.toAssocList.toList = l
@[simp]
theorem Batteries.AssocList.toList_toAssocList {α : Type u_1} {β : Type u_2} (l : ) :
l.toList.toAssocList = l
@[simp]
theorem List.length_toAssocList {α : Type u_1} {β : Type u_2} (l : List (α × β)) :
l.toAssocList.length = l.length
def Batteries.AssocList.beq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] :

Implementation of == on AssocList.

Equations
Instances For
instance Batteries.AssocList.instBEq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] :

Boolean equality for AssocList. (This relation cares about the ordering of the key-value pairs.)

Equations
• Batteries.AssocList.instBEq = { beq := Batteries.AssocList.beq }
@[simp]
theorem Batteries.AssocList.beq_nil₂ {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] :
(Batteries.AssocList.nil == Batteries.AssocList.nil) = true
@[simp]
theorem Batteries.AssocList.beq_nil_cons {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : } [BEq α] [BEq β] :
(Batteries.AssocList.nil == ) = false
@[simp]
theorem Batteries.AssocList.beq_cons_nil {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : } [BEq α] [BEq β] :
( == Batteries.AssocList.nil) = false
@[simp]
theorem Batteries.AssocList.beq_cons₂ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : } {a' : α} {b' : β} {t' : } [BEq α] [BEq β] :
( == Batteries.AssocList.cons a' b' t') = (a == a' && b == b' && t == t')
instance Batteries.AssocList.instLawfulBEq {α : Type u_1} {β : Type u_2} [BEq α] [] [BEq β] [] :
Equations
• =
theorem Batteries.AssocList.beq_eq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] {l : } {m : } :
(l == m) = (l.toList == m.toList)