# 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

- Batteries.DList.lazy_ofList l = { apply := fun (xs : List α) => l.get ++ xs, invariant := ⋯ }

## Instances For

theorem
Batteries.DList.toList_ofList
{α : Type u}
(l : List α)
:

(Batteries.DList.ofList l).toList = l

theorem
Batteries.DList.ofList_toList
{α : Type u}
(l : Batteries.DList α)
:

Batteries.DList.ofList l.toList = l

theorem
Batteries.DList.toList_singleton
{α : Type u}
(x : α)
:

(Batteries.DList.singleton x).toList = [x]

theorem
Batteries.DList.toList_append
{α : Type u}
(l₁ : Batteries.DList α)
(l₂ : Batteries.DList α)
:

theorem
Batteries.DList.toList_cons
{α : Type u}
(x : α)
(l : Batteries.DList α)
:

(Batteries.DList.cons x l).toList = x :: l.toList