max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/option): add optionT monad transformer

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-22 11:34:04 -07:00
parent 599916c352
commit 989e20a5d3
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
library/init/option.lean
View file

@ -43,3 +43,19 @@ definition option_orelse {A : Type} : option A → option A → option A
definition option_is_alternative [instance] {A : Type} : alternative option :=
alternative.mk @option_fmap @some (@fapp _ _) @none @option_orelse
definition optionT (m : Type → Type) [monad m] (A : Type) :=
m (option A)
inline definition optionT_fmap {m : Type → Type} [monad m] {A B : Type} (f : A → B) (e : optionT m A) : optionT m B :=
@monad.bind m _ _ _ e (λ a : option A, option.cases_on a (return none) (λ a, return (some (f a))))
inline definition optionT_bind {m : Type → Type} [monad m] {A B : Type} (a : optionT m A) (b : A → optionT m B)
: optionT m B :=
@monad.bind m _ _ _ a (λ a : option A, option.cases_on a (return none) (λ a, b a))
inline definition optionT_return {m : Type → Type} [monad m] {A : Type} (a : A) : optionT m A :=
@monad.ret m _ _ (some a)
definition optionT_is_monad [instance] {m : Type → Type} [monad m] {A : Type} : monad (optionT m) :=
monad.mk (@optionT_fmap m _) (@optionT_return m _) (@optionT_bind m _)