Skip to content

Commit

Permalink
chore: bump Std4 (#6695)
Browse files Browse the repository at this point in the history
The file [`Mathlib.Util.Pickle`](leanprover-community/batteries#211) has been upstreamed to std4, as has the declaration [`String.count`](leanprover-community/batteries#220).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
  • Loading branch information
semorrison and semorrison committed Aug 21, 2023
1 parent c6e395d commit 8854804
Show file tree
Hide file tree
Showing 6 changed files with 3 additions and 54 deletions.
1 change: 0 additions & 1 deletion Mathlib.lean
Expand Up @@ -3420,7 +3420,6 @@ import Mathlib.Util.IncludeStr
import Mathlib.Util.LongNames
import Mathlib.Util.MemoFix
import Mathlib.Util.PiNotation
import Mathlib.Util.Pickle
import Mathlib.Util.Qq
import Mathlib.Util.SleepHeartbeats
import Mathlib.Util.Superscript
Expand Down
4 changes: 0 additions & 4 deletions Mathlib/Data/String/Defs.lean
Expand Up @@ -45,10 +45,6 @@ def mapTokens (c : Char) (f : String → String) : String → String :=
intercalate (singleton c) ∘ List.map f ∘ (·.split (· = c))
#align string.map_tokens String.mapTokens

/-- Count the occurrences of a character in a string. -/
def count (s : String) (c : Char) : Nat :=
s.foldl (fun n d => if d = c then n + 1 else n) 0

/-- `getRest s t` returns `some r` if `s = t ++ r`.
If `t` is not a prefix of `s`, it returns `none`. -/
def getRest (s t : String) : Option String :=
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/LibrarySearch.lean
Expand Up @@ -3,7 +3,7 @@ Copyright (c) 2021 Gabriel Ebner. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner, Scott Morrison
-/
import Mathlib.Util.Pickle
import Std.Util.Pickle
import Mathlib.Tactic.Cache
import Mathlib.Tactic.SolveByElim
import Mathlib.Data.MLList.Heartbeats
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Rewrites.lean
Expand Up @@ -3,7 +3,7 @@ Copyright (c) 2023 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import Mathlib.Util.Pickle
import Std.Util.Pickle
import Mathlib.Data.MLList.Heartbeats
import Mathlib.Lean.Meta.DiscrTree
import Mathlib.Tactic.Cache
Expand Down
46 changes: 0 additions & 46 deletions Mathlib/Util/Pickle.lean

This file was deleted.

2 changes: 1 addition & 1 deletion lake-manifest.json
Expand Up @@ -36,7 +36,7 @@
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
"rev": "49353fa54abdac7221fe27f7b57a6ed9ff559d5c",
"rev": "61a6507eff4dd71c01e0c7e194bc569d4719a6d3",
"opts": {},
"name": "std",
"inputRev?": "main",
Expand Down

0 comments on commit 8854804

Please sign in to comment.