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.
Instances For
The apply
function of a DList
is completely determined by the list apply []
.
Equations
- Batteries.DList.instEmptyCollection = { emptyCollection := Batteries.DList.empty }
Equations
- Batteries.DList.instAppend = { append := Batteries.DList.append }