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} : AssocList α β

  An empty list

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

  Add a key, value pair to the list

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

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

def Batteries.AssocList.toList {α : Type u_1} {β : Type u_2} : AssocList α β → 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.

instance Batteries.AssocList.instEmptyCollection {α : Type u_1} {β : Type u_2} : EmptyCollection (AssocList α β)

@[simp]

theorem Batteries.AssocList.empty_eq {α : Type u_1} {β : Type u_2} : ∅ = nil

def Batteries.AssocList.isEmpty {α : Type u_1} {β : Type u_2} : AssocList α β → Bool

O(1). Is the list empty?

@[simp]

theorem Batteries.AssocList.isEmpty_eq {α : Type u_1} {β : Type u_2} (l : AssocList α β) : l.isEmpty = l.toList.isEmpty

def Batteries.AssocList.length {α : Type u_1} {β : Type u_2} (L : AssocList α β) : Nat

The number of entries in an AssocList.

@[simp]

theorem Batteries.AssocList.length_nil {α : Type u_1} {β : Type u_2} : nil.length = 0

@[simp]

theorem Batteries.AssocList.length_cons {α✝ : Type u_1} {a : α✝} {β✝ : Type u_2} {b : β✝} {t : AssocList α✝ β✝} : (cons a b t).length = t.length + 1

theorem Batteries.AssocList.length_toList {α : Type u_1} {β : Type u_2} (l : AssocList α β) : 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} [Monad m] (f : δ → α → β → m δ) (init : δ) : AssocList α β → m δ

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

@[simp]

theorem Batteries.AssocList.foldlM_eq {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [Monad m] (f : δ → α → β → m δ) (init : δ) (l : AssocList α β) : foldlM f 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 : AssocList α β) : δ

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

@[simp]

theorem Batteries.AssocList.foldl_eq {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δ → α → β → δ) (init : δ) (l : AssocList α β) : foldl 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 : AssocList α β) : List (α × β)

Optimized version of toList.

@[csimp]

theorem Batteries.AssocList.toList_eq_toListTR : @toList = @toListTR

@[specialize #[]]

def Batteries.AssocList.forM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] (f : α → β → m PUnit) : AssocList α β → m PUnit

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

@[simp]

theorem Batteries.AssocList.forM_eq {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] (f : α → β → m PUnit) (l : AssocList α β) : forM 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 : α → δ) : AssocList α β → AssocList δ β

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

@[simp]

theorem Batteries.AssocList.toList_mapKey {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : α → δ) (l : AssocList α β) : (mapKey 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} {α✝¹ : Type u_2} {f : α✝ → α✝¹} {β✝ : Type u_3} {l : AssocList α✝ β✝} : (mapKey f l).length = l.length

def Batteries.AssocList.mapVal {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : α → β → δ) : AssocList α β → AssocList α δ

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

@[simp]

theorem Batteries.AssocList.toList_mapVal {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : α → β → δ) (l : AssocList α β) : (mapVal 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} {β✝¹ : Type u_3} {f : α✝ → β✝ → β✝¹} {l : AssocList α✝ β✝} : (mapVal f l).length = l.length

@[specialize #[]]

def Batteries.AssocList.findEntryP? {α : Type u_1} {β : Type u_2} (p : α → β → Bool) : AssocList α β → Option (α × β)

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

@[simp]

theorem Batteries.AssocList.findEntryP?_eq {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (l : AssocList α β) : findEntryP? p 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 : AssocList α β) : Option (α × β)

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

@[simp]

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

def Batteries.AssocList.find? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) : AssocList α β → Option β

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

theorem Batteries.AssocList.find?_eq_findEntry? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : AssocList α β) : find? a l = Option.map (fun (x : α × β) => x.snd) (findEntry? a l)

@[simp]

theorem Batteries.AssocList.find?_eq {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : AssocList α β) : find? 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) : AssocList α β → Bool

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

@[simp]

theorem Batteries.AssocList.any_eq {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (l : AssocList α β) : any p 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) : AssocList α β → Bool

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

@[simp]

theorem Batteries.AssocList.all_eq {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (l : AssocList α β) : all p 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 : AssocList α β) : Prop

Returns true if every entry in the list satisfies p.

@[inline]

def Batteries.AssocList.contains {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : AssocList α β) : Bool

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

@[simp]

theorem Batteries.AssocList.contains_eq {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : AssocList α β) : contains a l = l.toList.any fun (x : α × β) => x.fst == a

def Batteries.AssocList.replace {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (b : β) : AssocList α β → AssocList α β

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

@[simp]

theorem Batteries.AssocList.toList_replace {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (b : β) (l : AssocList α β) : (replace 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 : AssocList α β✝} [BEq α] {a : α} : (replace a b l).length = l.length

@[specialize #[]]

def Batteries.AssocList.eraseP {α : Type u_1} {β : Type u_2} (p : α → β → Bool) : AssocList α β → AssocList α β

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

@[simp]

theorem Batteries.AssocList.toList_eraseP {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (l : AssocList α β) : (eraseP p 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 : AssocList α β) : AssocList α β

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

@[simp]

theorem Batteries.AssocList.toList_erase {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : AssocList α β) : (erase 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 : α → β → β) : AssocList α β → AssocList α β

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.

@[simp]

theorem Batteries.AssocList.toList_modify {α : Type u_1} {β : Type u_2} {f : α → β → β} [BEq α] (a : α) (l : AssocList α β) : (modify a f 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 : AssocList α β✝} [BEq α] {a : α} : (modify a f l).length = l.length

@[specialize #[]]

def Batteries.AssocList.forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [Monad m] (as : AssocList α β) (init : δ) (f : α × β → δ → m (ForInStep δ)) : m δ

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

instance Batteries.AssocList.instForInProdOfMonad {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] : ForIn m (AssocList α β) (α × β)

@[simp]

theorem Batteries.AssocList.forIn_eq {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [Monad m] (l : AssocList α β) (init : δ) (f : α × β → δ → m (ForInStep δ)) : forIn l init f = forIn l.toList init f

def Batteries.AssocList.pop? {α : Type u_1} {β : Type u_2} : AssocList α β → Option ((α × β) × AssocList α β)

Split the list into head and tail, if possible.

instance Batteries.AssocList.instToStream {α : Type u_1} {β : Type u_2} : Std.ToStream (AssocList α β) (AssocList α β)

instance Batteries.AssocList.instStreamProd {α : Type u_1} {β : Type u_2} : Std.Stream (AssocList α β) (α × β)

def List.toAssocList {α : Type u_1} {β : Type u_2} : List (α × β) → Batteries.AssocList α β

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

@[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 : AssocList α β) : 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 β] : AssocList α β → AssocList α β → Bool

Implementation of == on AssocList.

instance Batteries.AssocList.instBEq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] : BEq (AssocList α β)

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

@[simp]

theorem Batteries.AssocList.beq_nil₂ {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] : (nil == nil) = true

@[simp]

theorem Batteries.AssocList.beq_nil_cons {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : AssocList α β} [BEq α] [BEq β] : (nil == cons a b t) = false

@[simp]

theorem Batteries.AssocList.beq_cons_nil {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : AssocList α β} [BEq α] [BEq β] : (cons a b t == nil) = false

@[simp]

theorem Batteries.AssocList.beq_cons₂ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : AssocList α β} {a' : α} {b' : β} {t' : AssocList α β} [BEq α] [BEq β] : (cons a b t == cons a' b' t') = (a == a' && b == b' && t == t')

instance Batteries.AssocList.instLawfulBEq {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] : LawfulBEq (AssocList α β)

theorem Batteries.AssocList.beq_eq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] {l m : AssocList α β} : (l == m) = (l.toList == m.toList)