Commit 2024-10-16 01:59 a003b0ef

View on Github →

chore: bump Batteries (upstreamed DList) (#17791)

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Data/DList/Basic.lean

deleted def Batteries.DList.join

deleted theorem Batteries.DList_lazy

deleted theorem Batteries.DList_singleton

Deleted Mathlib/Data/DList/Defs.lean

deleted def Batteries.DList.lazy_ofList

deleted theorem Batteries.DList.ofList_toList

deleted theorem Batteries.DList.toList_append

deleted theorem Batteries.DList.toList_cons

deleted theorem Batteries.DList.toList_empty

deleted theorem Batteries.DList.toList_ofList

deleted theorem Batteries.DList.toList_push

deleted theorem Batteries.DList.toList_singleton

Modified Mathlib/Data/DList/Instances.lean

Modified Mathlib/Data/Seq/WSeq.lean

Modified lake-manifest.json