core / data.dlist - mathlib docs

structure dlist (α : Type u) :

Type u

apply : list α → list α
invariant : ∀ (l : list α), self.apply l = self.apply list.nil ++ 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.

source

def dlist.of_list {α : Type u} (l : list α) :

dlist α

Convert a list to a dlist

Equations

dlist.of_list l = {apply := append l, invariant := _}

source

def dlist.lazy_of_list {α : Type u} (l : thunk (list α)) :

dlist α

Convert a lazily-evaluated list to a dlist

Equations

dlist.lazy_of_list l = {apply := λ (xs : list α), l () ++ xs, invariant := _}

source

def dlist.to_list {α : Type u} :

dlist α → list α

Convert a dlist to a list

Equations

{apply := xs, invariant := _x}.to_list = xs list.nil

source

def dlist.empty {α : Type u} :

dlist α

Create a dlist containing no elements

Equations

dlist.empty = {apply := id (list α), invariant := _}

source

def dlist.singleton {α : Type u} (x : α) :

dlist α

Create dlist with a single element

Equations

dlist.singleton x = {apply := list.cons x, invariant := _}

source

def dlist.cons {α : Type u} (x : α) :

dlist α → dlist α

O(1) Prepend a single element to a dlist

Equations

dlist.cons x {apply := xs, invariant := h} = {apply := list.cons x ∘ xs, invariant := _}

source

def dlist.concat {α : Type u} (x : α) :

dlist α → dlist α

O(1) Append a single element to a dlist

Equations

dlist.concat x {apply := xs, invariant := h} = {apply := xs ∘ list.cons x, invariant := _}

source

@[protected]

def dlist.append {α : Type u} :

dlist α → dlist α → dlist α

O(1) Append dlists

Equations

{apply := xs, invariant := h₁}.append {apply := ys, invariant := h₂} = {apply := xs ∘ ys, invariant := _}

source

@[protected, instance]

def dlist.has_append {α : Type u} :

has_append (dlist α)

Equations

dlist.has_append = {append := dlist.append α}

source

theorem dlist.to_list_of_list {α : Type u} (l : list α) :

(dlist.of_list l).to_list = l

source

theorem dlist.of_list_to_list {α : Type u} (l : dlist α) :

dlist.of_list l.to_list = l

source

theorem dlist.to_list_empty {α : Type u} :

dlist.empty.to_list = list.nil

source

theorem dlist.to_list_singleton {α : Type u} (x : α) :

(dlist.singleton x).to_list = [x]

source

theorem dlist.to_list_append {α : Type u} (l₁ l₂ : dlist α) :

(l₁ ++ l₂).to_list = l₁.to_list ++ l₂.to_list

source

theorem dlist.to_list_cons {α : Type u} (x : α) (l : dlist α) :

(dlist.cons x l).to_list = x :: l.to_list

source

theorem dlist.to_list_concat {α : Type u} (x : α) (l : dlist α) :

(dlist.concat x l).to_list = l.to_list ++ [x]