Commit 2023-06-18 08:20 a88976af

View on Github →

feat: port Data.DList from Lean core (#1498)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/DList/Basic.lean

deleted def Std.DList.lazy_ofList

deleted theorem Std.DList.ofList_toList

deleted theorem Std.DList.toList_ofList

Created Mathlib/Data/DList/Defs.lean

added def Std.DList.lazy_ofList

added theorem Std.DList.ofList_toList

added theorem Std.DList.toList_append

added theorem Std.DList.toList_cons

added theorem Std.DList.toList_empty

added theorem Std.DList.toList_ofList

added theorem Std.DList.toList_push

added theorem Std.DList.toList_singleton

Modified Mathlib/Data/DList/Instances.lean