# Documentation

Mathlib.Data.DList.Basic

# Difference list #

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

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 concat operations on lists, making it useful for append-heavy uses such as logging and pretty printing.

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

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

Equations
def Std.DList.lazy_ofList {α : Type u_1} (l : Thunk (List α)) :

Convert a lazily-evaluated List to a DList

Equations
• = { apply := fun xs => ++ xs, invariant := (_ : ∀ (t : List α), ++ t = ++ [] ++ t) }
@[simp]
theorem Std.DList_singleton {α : Type u_1} {a : α} :
= Std.DList.lazy_ofList { fn := fun x => [a] }
@[simp]
theorem Std.DList_lazy {α : Type u_1} {l : List α} :
Std.DList.lazy_ofList { fn := fun x => l } =
theorem Std.DList.toList_ofList {α : Type u_1} (l : List α) :
theorem Std.DList.ofList_toList {α : Type u_1} (l : ) :