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

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

Convert a lazily-evaluated List to a DList

Equations

• Std.DList.lazy_ofList l = { apply := fun (xs : List α) => Thunk.get l ++ xs, invariant := (_ : ∀ (t : List α), Thunk.get l ++ t = Thunk.get l ++ [] ++ t) }

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

theorem Std.DList.ofList_toList {α : Type u} (l : Std.DList α) : Std.DList.ofList (Std.DList.toList l) = l

theorem Std.DList.toList_empty {α : Type u} : Std.DList.toList Std.DList.empty = []

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

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

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

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