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.of_list and DList.to_list.

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • Std.instInhabitedDList = { default := Std.DList.empty }