"Run" a
DList
by appending it on the right by aList α
to get anotherList α
.
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
Equations
- Std.DList.instEmptyCollectionDList = { emptyCollection := Std.DList.empty }
O(apply())
. Convert a DList α
into a List α
by running the apply
function.
Equations
- Std.DList.toList x = match x with | { apply := f, invariant := invariant } => f []
O(1)
(apply
is O(1)
). Append two DList α
.
O(1)
(apply
is O(1)
). Append an element at the end of a DList α
.