From ca20bb112fd4555e3e14454e584aca7e49cc0f68 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Feb 2020 12:10:52 -0800 Subject: [PATCH] feat: add helper --- src/Init/Data/List/Control.lean | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index 3a0c8d36f6..78a499d9b7 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -128,8 +128,17 @@ def allM {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : Lis | false => pure false @[specialize] -def findM? {m : Type → Type} [Monad m] {α : Type} (p : α → m Bool) : List α → m (Option α) +def findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : List α → m (Option α) | [] => pure none | a::as => condM (p a) (pure (some a)) (findM? as) +@[specialize] +def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → m (Option β) +| [] => pure none +| a::as => do + b? ← f a; + match b? with + | some b => pure b + | none => findSomeM? as + end List