mathlib documentation

data.dlist.instances

def dlist.list_equiv_dlist (α : Type u_1) :
list α dlist α

The natural equivalence between lists and difference lists, using dlist.of_list and dlist.to_list.

Equations
@[instance]
def dlist.inhabited {α : Type u_1} :

Equations