Documentation

Mathlib.Data.DList.Instances

Traversable instance for DLists #

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

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

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

Equations
    Instances For
      source
      🔸 coverage
      instance Batteries.instTraversableDList :
      Traversable DList
      Equations
        source
        📐 coverage
        instance Batteries.instLawfulTraversableDList :
        LawfulTraversable DList