Traversable instance for dlists #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 α}