Difference list #
This file provides a few results about dlist, which is defined in core Lean.
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 concat operations on lists, making it
useful for append-heavy uses such as logging and pretty printing.
Concatenates a list of difference lists to form a single difference list. Similar to
list.join.
Equations
- dlist.join (x :: xs) = x ++ dlist.join xs
- dlist.join list.nil = dlist.empty
@[simp]
theorem
dlist_singleton
{α : Type u_1}
{a : α} :
dlist.singleton a = dlist.lazy_of_list (λ («_» : unit), [a])
@[simp]
theorem
dlist_lazy
{α : Type u_1}
{l : list α} :
dlist.lazy_of_list (λ («_» : unit), l) = dlist.of_list l