Skip to content

Commit

Permalink
chore: bump Std to #253 (#7113)
Browse files Browse the repository at this point in the history
Bump PR for leanprover-community/batteries#253



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
  • Loading branch information
semorrison and semorrison committed Sep 12, 2023
1 parent 6de5329 commit d0e5669
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 9 deletions.
9 changes: 1 addition & 8 deletions Mathlib/Control/Basic.lean
Expand Up @@ -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"

Expand Down Expand Up @@ -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 : TypeType} [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 : β → γ} :
Expand Down
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": "e8c27f7d90ee71470558efd1bc197fe55068c748",
"rev": "2a10db96d0ea1c00d0b30d2bbcea7e7b4584ffba",
"opts": {},
"name": "std",
"inputRev?": "main",
Expand Down

0 comments on commit d0e5669

Please sign in to comment.