# Documentation

## Batteries.Data.DList

structure Batteries.DList (α : 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.

• apply : List αList α

"Run" a DList by appending it on the right by a List α to get another List α.

• invariant : ∀ (l : List α), self.apply l = self.apply [] ++ l

The apply function of a DList is completely determined by the list apply [].

Instances For
theorem Batteries.DList.invariant {α : Type u} (self : ) (l : List α) :
self.apply l = self.apply [] ++ l

The apply function of a DList is completely determined by the list apply [].

def Batteries.DList.ofList {α : Type u} (l : List α) :

O(1) (apply is O(|l|)). Convert a List α into a DList α.

Equations
• = { apply := fun (x : List α) => l ++ x, invariant := }
Instances For

O(1) (apply is O(1)). Return an empty DList α.

Equations
• Batteries.DList.empty = { apply := id, invariant := }
Instances For
Equations
• Batteries.DList.instEmptyCollection = { emptyCollection := Batteries.DList.empty }
def Batteries.DList.toList {α : Type u} :
List α

O(apply()). Convert a DList α into a List α by running the apply function.

Equations
• x.toList = match x with | { apply := f, invariant := invariant } => f []
Instances For
def Batteries.DList.singleton {α : Type u} (a : α) :

O(1) (apply is O(1)). A DList α corresponding to the list [a].

Equations
• = { apply := fun (t : List α) => a :: t, invariant := }
Instances For
def Batteries.DList.cons {α : Type u} :
α

O(1) (apply is O(1)). Prepend a on a DList α.

Equations
• = match x✝, x with | a, { apply := f, invariant := h } => { apply := fun (t : List α) => a :: f t, invariant := }
Instances For

O(1) (apply is O(1)). Append two DList α.

Equations
• x✝.append x = match x✝, x with | { apply := f, invariant := h₁ }, { apply := g, invariant := h₂ } => { apply := f g, invariant := }
Instances For
def Batteries.DList.push {α : Type u} :
α

O(1) (apply is O(1)). Append an element at the end of a DList α.

Equations
• x✝.push x = match x✝, x with | { apply := f, invariant := h }, a => { apply := fun (t : List α) => f (a :: t), invariant := }
Instances For
instance Batteries.DList.instAppend {α : Type u} :
Equations
• Batteries.DList.instAppend = { append := Batteries.DList.append }