mathlib documentation

core / data.dlist

structure dlist (α : Type u) :
Type u

A difference list is a function that, given a list, returns the original contents of the difference list prepended to the given list.

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 dlist.of_list {α : Type u} (l : list α) :

Convert a list to a dlist

Equations
def dlist.lazy_of_list {α : Type u} (l : thunk (list α)) :

Convert a lazily-evaluated list to a dlist

Equations
def dlist.to_list {α : Type u} :
dlist αlist α

Convert a dlist to a list

Equations
def dlist.empty {α : Type u} :

Create a dlist containing no elements

Equations
def dlist.singleton {α : Type u} (x : α) :

Create dlist with a single element

Equations
def dlist.cons {α : Type u} (x : α) :
dlist αdlist α

O(1) Prepend a single element to a dlist

Equations
def dlist.concat {α : Type u} (x : α) :
dlist αdlist α

O(1) Append a single element to a dlist

Equations
@[protected]
def dlist.append {α : Type u} :
dlist αdlist αdlist α

O(1) Append dlists

Equations
@[protected, instance]
def dlist.has_append {α : Type u} :
Equations
theorem dlist.to_list_of_list {α : Type u} (l : list α) :
theorem dlist.of_list_to_list {α : Type u} (l : dlist α) :
theorem dlist.to_list_singleton {α : Type u} (x : α) :
theorem dlist.to_list_append {α : Type u} (l₁ l₂ : dlist α) :
(l₁ ++ l₂).to_list = l₁.to_list ++ l₂.to_list
theorem dlist.to_list_cons {α : Type u} (x : α) (l : dlist α) :
theorem dlist.to_list_concat {α : Type u} (x : α) (l : dlist α) :