Difference list

This file provides a few results about DList, which is defined in Batteries.

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.

def Batteries.DList.join {α : Type u_1} : List (Batteries.DList α) → Batteries.DList α

Concatenates a list of difference lists to form a single difference list. Similar to List.join.

Equations

• Batteries.DList.join [] = Batteries.DList.empty
• Batteries.DList.join (x_1 :: xs) = x_1 ++ Batteries.DList.join xs

@[simp]

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

@[simp]

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