Commit 2022-11-25 20:16 be9c254d

View on Github →

feat: port: Data.DList.Basic (#616) To review: had to cross port lazy_OfList from Lean core, naming is odd in Std (Std.DList rather than Std.Data.DList Also not clear about naming choices... ported from 8c53048add6ffacdda0b36c4917bfe37e209b0ba

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/DList/Basic.lean

added def Std.DList.join

added def Std.DList.lazy_ofList

added theorem Std.DList_lazy

added theorem Std.DList_singleton