structure Batteries.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 push 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 [].

theorem Batteries.DList.invariant {α : Type u} (self : Batteries.DList α) (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 α) : Batteries.DList α

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

Equations

• Batteries.DList.ofList l = { apply := fun (x : List α) => l ++ x, invariant := ⋯ }

def Batteries.DList.empty {α : Type u} : Batteries.DList α

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

Equations

• Batteries.DList.empty = { apply := id, invariant := ⋯ }

instance Batteries.DList.instEmptyCollection {α : Type u} : EmptyCollection (Batteries.DList α)

Equations

• Batteries.DList.instEmptyCollection = { emptyCollection := Batteries.DList.empty }

instance Batteries.DList.instInhabited {α : Type u} : Inhabited (Batteries.DList α)

Equations

• Batteries.DList.instInhabited = { default := Batteries.DList.empty }

def Batteries.DList.toList {α : Type u} : Batteries.DList α → List α

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

Equations

• { apply := f, invariant := invariant }.toList = f []

def Batteries.DList.singleton {α : Type u} (a : α) : Batteries.DList α

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

Equations

• Batteries.DList.singleton a = { apply := fun (t : List α) => a :: t, invariant := ⋯ }

def Batteries.DList.cons {α : Type u} : α → Batteries.DList α → Batteries.DList α

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

Equations

• Batteries.DList.cons x { apply := f, invariant := h } = { apply := fun (t : List α) => x :: f t, invariant := ⋯ }

def Batteries.DList.append {α : Type u} : Batteries.DList α → Batteries.DList α → Batteries.DList α

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

Equations

• { apply := f, invariant := h₁ }.append { apply := g, invariant := h₂ } = { apply := f ∘ g, invariant := ⋯ }

def Batteries.DList.push {α : Type u} : Batteries.DList α → α → Batteries.DList α

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

Equations

• { apply := f, invariant := h }.push x = { apply := fun (t : List α) => f (x :: t), invariant := ⋯ }

instance Batteries.DList.instAppend {α : Type u} : Append (Batteries.DList α)

Equations

• Batteries.DList.instAppend = { append := Batteries.DList.append }

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

Convert a lazily-evaluated List to a DList

Equations

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

@[deprecated Batteries.DList.ofThunk]

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

Alias of Batteries.DList.ofThunk.

---

Convert a lazily-evaluated List to a DList

Equations

• @Batteries.DList.lazy_ofList = @Batteries.DList.ofThunk

def Batteries.DList.join {α : Type u_1} : List (Batteries.DList α) → Batteries.DList α

Concatenates a list of difference lists to form a single difference list. Similar to List.join.

Equations

• Batteries.DList.join [] = Batteries.DList.empty
• Batteries.DList.join (x_1 :: xs) = x_1 ++ Batteries.DList.join xs