ink

structure Std.DList (α : Type u) : Type u

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

  apply : List α → List α

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

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

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.

ink

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

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

Equations

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

ink

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

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

Equations

• Std.DList.empty = { apply := id, invariant := (_ : ∀ (x : List α), id x = id x) }

ink

instance Std.DList.instEmptyCollectionDList {α : Type u} : EmptyCollection (Std.DList α)

Equations

• Std.DList.instEmptyCollectionDList = { emptyCollection := Std.DList.empty }

ink

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

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

Equations

• Std.DList.toList x = match x with | { apply := f, invariant := invariant } => f []

ink

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

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

Equations

• Std.DList.singleton a = { apply := fun t => a :: t, invariant := (_ : ∀ (x : List α), (fun t => a :: t) x = (fun t => a :: t) x) }

ink

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

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

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

Equations

• Std.DList.append x x = match x, x with | { apply := f, invariant := h₁ }, { apply := g, invariant := h₂ } => { apply := f ∘ g, invariant := (_ : ∀ (t : List α), f (g t) = f (g []) ++ t) }

ink

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

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

Equations

• Std.DList.push x x = match x, x with | { apply := f, invariant := h }, a => { apply := fun t => f (a :: t), invariant := (_ : ∀ (t : List α), f (a :: t) = f [a] ++ t) }

ink

instance Std.DList.instAppendDList {α : Type u} : Append (Std.DList α)

Equations

• Std.DList.instAppendDList = { append := Std.DList.append }