mathlib3 documentation


Difference list #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

def dlist.join {α : Type u_1} :

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

theorem dlist_singleton {α : Type u_1} {a : α} :
theorem dlist_lazy {α : Type u_1} {l : list α} :