Commit 2023-01-31 10:56 42aaa1f2

View on Github →

feat: Port Data.DList.Instances (#1932)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/DList/Basic.lean

added theorem Std.DList.ofList_toList

added theorem Std.DList.toList_ofList

Created Mathlib/Data/DList/Instances.lean

added def Std.DList.listEquivDList