Traversable instance for DLists

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

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

The natural equivalence between lists and difference lists, using DList.ofList and DList.toList.

Equations

• Batteries.DList.listEquivDList α = { toFun := Batteries.DList.ofList, invFun := Batteries.DList.toList, left_inv := ⋯, right_inv := ⋯ }

instance Batteries.instTraversableDList : Traversable Batteries.DList

Equations

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

instance Batteries.instLawfulTraversableDList : LawfulTraversable Batteries.DList

Equations

• Batteries.instLawfulTraversableDList = ⋯

instance Batteries.instInhabitedDList_mathlib {α : Type u_2} : Inhabited (Batteries.DList α)

Equations

• Batteries.instInhabitedDList_mathlib = { default := Batteries.DList.empty }