instLawfulTraversableDList — Mathlib

English

The difference list type Batteries.DList is a lawful traversable structure, i.e., it supports lawful traversable operations via the equivalence with lists.

Русский

Тип Batteries.DList является законнойTraversable структурой через эквиваленцию со списками.

LaTeX

$$$\\text{Batteries.DList}.instLawfulTraversableDList : \\text{LawfulTraversable }\\mathrm{DList}$$$

Lean4

instance : LawfulTraversable DList :=
  Equiv.isLawfulTraversable DList.listEquivDList

Похожие утверждения