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 := _}
@[instance]
@[instance]
@[instance]
Equations
- dlist.inhabited = {default := dlist.empty α}