Traversable instance for dlists #
This file provides the equivalence between list α
and dlist α
and the traversable instance
for dlist
.
The natural equivalence between lists and difference lists, using
dlist.of_list
and dlist.to_list
.
Equations
- dlist.list_equiv_dlist α = {to_fun := dlist.of_list α, inv_fun := dlist.to_list α, left_inv := _, right_inv := _}
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- dlist.inhabited = {default := dlist.empty α}