chore: bump Std to #253 (#7113)

Bump PR for leanprover-community/batteries#253



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib/Control/Basic.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl
 import Mathlib.Init.Control.Combinators
 import Mathlib.Tactic.CasesM
 import Mathlib.Tactic.Attr.Core
+import Std.Data.List.Basic
 
 #align_import control.basic from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
 
@@ -77,14 +78,6 @@ variable {m : Type u → Type v} [Monad m] [LawfulMonad m]
 
 open List
 
-/-- A generalization of `List.partition` which partitions the list according to a monadic
-predicate. `List.partition` corresponds to the case where `f = Id`. -/
-def List.partitionM {f : Type → Type} [Monad f] {α : Type} (p : α → f Bool) :
-    List α → f (List α × List α)
-  | [] => pure ([], [])
-  | x :: xs => condM (p x)
-    (Prod.map (cons x) id <$> List.partitionM p xs)
-    (Prod.map id (cons x) <$> List.partitionM p xs)
 #align list.mpartition List.partitionM
 
 theorem map_bind (x : m α) {g : α → m β} {f : β → γ} :

lake-manifest.json

@@ -36,7 +36,7 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "e8c27f7d90ee71470558efd1bc197fe55068c748",
+    "rev": "2a10db96d0ea1c00d0b30d2bbcea7e7b4584ffba",
     "opts": {},
     "name": "std",
     "inputRev?": "main",