Difference list

This file provides a few results about DList.

A difference list is a function that, given a list, returns the original content of the difference list prepended to the given list. It is useful to represent elements of a given type as a₁ + ... + aₙ where + : α → α → α is any operation, without actually computing.

This structure supports O(1) append and push operations on lists, making it useful for append-heavy uses such as logging and pretty printing.

theorem Batteries.DList.toList_ofList {α : Type u_1} (l : List α) : (ofList l).toList = l

theorem Batteries.DList.ofList_toList {α : Type u_1} (l : DList α) : ofList l.toList = l

theorem Batteries.DList.toList_empty {α : Type u_1} : empty.toList = []

theorem Batteries.DList.toList_singleton {α : Type u_1} (x : α) : (singleton x).toList = [x]

theorem Batteries.DList.toList_append {α : Type u_1} (l₁ l₂ : DList α) : (l₁ ++ l₂).toList = l₁.toList ++ l₂.toList

theorem Batteries.DList.toList_cons {α : Type u_1} (x : α) (l : DList α) : (cons x l).toList = x :: l.toList

theorem Batteries.DList.toList_push {α : Type u_1} (x : α) (l : DList α) : (l.push x).toList = l.toList ++ [x]

@[simp]

theorem Batteries.DList.singleton_eq_ofThunk {α : Type u_1} {a : α} : singleton a = ofThunk { fn := fun (x : Unit) => [a] }

@[simp]

theorem Batteries.DList.ofThunk_coe {α : Type u_1} {l : List α} : ofThunk { fn := fun (x : Unit) => l } = ofList l

@[deprecated Batteries.DList.singleton_eq_ofThunk (since := "2024-10-16")]

theorem Batteries.DList.DList_singleton {α : Type u_1} {a : α} : singleton a = ofThunk { fn := fun (x : Unit) => [a] }

Alias of Batteries.DList.singleton_eq_ofThunk.

@[deprecated Batteries.DList.ofThunk_coe (since := "2024-10-16")]

theorem Batteries.DList.DList_lazy {α : Type u_1} {l : List α} : ofThunk { fn := fun (x : Unit) => l } = ofList l

Alias of Batteries.DList.ofThunk_coe.