Documentation

Mathlib.Data.DList.Defs

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.

Convert a lazily-evaluated List to a DList

Equations
Instances For
    theorem Batteries.DList.toList_ofList {α : Type u} (l : List α) :
    theorem Batteries.DList.toList_empty {α : Type u} :
    Batteries.DList.empty.toList = []
    theorem Batteries.DList.toList_append {α : Type u} (l₁ : Batteries.DList α) (l₂ : Batteries.DList α) :
    (l₁ ++ l₂).toList = l₁.toList ++ l₂.toList
    theorem Batteries.DList.toList_cons {α : Type u} (x : α) (l : Batteries.DList α) :
    (Batteries.DList.cons x l).toList = x :: l.toList
    theorem Batteries.DList.toList_push {α : Type u} (x : α) (l : Batteries.DList α) :
    (l.push x).toList = l.toList ++ [x]