Documentation

Mathlib.Data.DList.Instances

Traversable instance for DLists #

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

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

Equations
Instances For
    Equations
    • Batteries.instInhabitedDList_mathlib = { default := Batteries.DList.empty }