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

dlist.list_equiv_dlist α = {to_fun := dlist.of_list α, inv_fun := dlist.to_list α, left_inv := _, right_inv := _}

@[instance]

def dlist.traversable :

traversable dlist

Equations

dlist.traversable = equiv.traversable dlist.list_equiv_dlist

@[instance]

def dlist.is_lawful_traversable :

is_lawful_traversable dlist

Equations

dlist.is_lawful_traversable = equiv.is_lawful_traversable dlist.list_equiv_dlist

@[instance]

def dlist.inhabited {α : Type u_1} :

inhabited (dlist α)

Equations

dlist.inhabited = {default := dlist.empty α}