mathlib3 documentation

data.dlist.instances

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.

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
@[protected, instance]
def dlist.inhabited {α : Type u_1} :
Equations