Traversable instance for DLists

This file provides the equivalence between List α and DList α and the traversable instance for DList.

ink

def Std.DList.listEquivDList (α : Type u_1) : List α ≃ Std.DList α

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

Equations

• One or more equations did not get rendered due to their size.

ink

instance Std.instTraversableDList : Traversable Std.DList

Equations

• Std.instTraversableDList = Equiv.traversable Std.DList.listEquivDList

ink

instance Std.instIsLawfulTraversableDListInstTraversableDList : IsLawfulTraversable Std.DList

Equations

• Std.instIsLawfulTraversableDListInstTraversableDList = Equiv.isLawfulTraversable Std.DList.listEquivDList

ink

instance Std.instInhabitedDList {α : Type u_1} : Inhabited (Std.DList α)

Equations

• Std.instInhabitedDList = { default := Std.DList.empty }