From 35b99aafb2e5042d90afca93e3125869ef0432ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Jun 2017 18:53:22 -0700 Subject: [PATCH] feat(library/init/category/combinators): add list.mfirst --- library/init/category/combinators.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/library/init/category/combinators.lean b/library/init/category/combinators.lean index 478f7b4179..5bc329cfb6 100644 --- a/library/init/category/combinators.lean +++ b/library/init/category/combinators.lean @@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura Monad combinators, as in Haskell's Control.Monad. -/ prelude -import init.category.monad init.data.list.basic +import init.category.monad init.category.alternative init.data.list.basic universes u v w def list.mmap {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m (list β) @@ -48,6 +48,10 @@ def list.mfoldr {m : Type u → Type v} [monad m] {s : Type u} {α : Type w} : ( s' ← list.mfoldr f s r, f h s' +def list.mfirst {m : Type u → Type v} [monad m] [alternative m] {α : Type w} {β : Type u} (f : α → m β) : list α → m β +| [] := failure +| (a::as) := f a <|> list.mfirst as + def when {m : Type → Type} [monad m] (c : Prop) [h : decidable c] (t : m unit) : m unit := ite c t (pure ())