Commit 2023-08-21 04:30 88548040

View on Github →

chore: bump Std4 (#6695) The file Mathlib.Util.Pickle has been upstreamed to std4, as has the declaration String.count.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/String/Defs.lean

deleted def String.count

Modified Mathlib/Tactic/LibrarySearch.lean

Modified Mathlib/Tactic/Rewrites.lean

Deleted Mathlib/Util/Pickle.lean

deleted def pickle

Modified lake-manifest.json