Difference list #
This file provides a few results about
DList, which is defined in
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
a₁ + ... + aₙ where
+ : α → α → α is any operation, without actually computing.
This structure supports
push operations on lists, making it
useful for append-heavy uses such as logging and pretty printing.