Commit 2023-09-27 03:37 2c8d12cc

View on Github →

chore: bump to std#260 (#7134)

Estimated changes

Modified Mathlib/Combinatorics/Composition.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.dropLast_cons_cons

deleted theorem List.enumFrom_cons

deleted theorem List.enumFrom_nil

deleted theorem List.find?_nil

deleted theorem List.foldlM_cons

deleted theorem List.foldlM_nil

deleted theorem List.foldl_cons

deleted theorem List.foldl_nil

deleted theorem List.foldr_cons

deleted theorem List.foldr_nil

deleted theorem List.intersperse_nil

deleted theorem List.take_zero

Modified Mathlib/Data/List/Chain.lean

Modified Mathlib/Data/List/EditDistance/Defs.lean

Modified Mathlib/Data/List/Indexes.lean

Modified Mathlib/Data/List/Zip.lean

deleted theorem List.length_zip

deleted theorem List.unzip_cons

deleted theorem List.unzip_nil

deleted theorem List.zipWith_cons_cons

deleted theorem List.zipWith_nil_left

deleted theorem List.zipWith_nil_right

deleted theorem List.zip_cons_cons

deleted theorem List.zip_nil_left

deleted theorem List.zip_nil_right

Modified Mathlib/Data/UnionFind.lean

Modified Mathlib/Data/Vector/Basic.lean

Modified lake-manifest.json