feat(init/data/option_t): option_t is a monad transformer
This commit is contained in:
parent
52e41ecd1d
commit
b28ff94780
1 changed files with 5 additions and 1 deletions
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.meta.interactive
|
||||
import init.meta.interactive init.category.transformers
|
||||
|
||||
universes u v
|
||||
|
||||
|
|
@ -66,3 +66,7 @@ instance {m : Type u → Type v} [monad m] : alternative (option_t m) :=
|
|||
|
||||
def option_t.lift {m : Type u → Type v} [monad m] {α : Type u} (a : m α) : option_t m α :=
|
||||
(some <$> a : m (option α))
|
||||
|
||||
instance option_t.monad_transformer : monad.monad_transformer option_t :=
|
||||
{ is_monad := @option_t.monad,
|
||||
monad_lift := @option_t.lift }
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue