Equations
- option_t.bind_cont f (option.some a) = (f a).run
- option_t.bind_cont f option.none = has_pure.pure option.none
Equations
- option_t.pure a = {run := has_pure.pure (option.some a)}
@[instance]
Equations
Equations
- ma.orelse mb = {run := ma.run >>= λ (_p : option α), option_t.orelse._match_1 mb _p}
- option_t.orelse._match_1 mb (option.some a) = has_pure.pure (option.some a)
- option_t.orelse._match_1 mb option.none = mb.run
Equations
Equations
- option_t.of_option o = {run := has_pure.pure o}
@[instance]
Equations
- option_t.alternative = {to_applicative := monad.to_applicative option_t.monad, to_has_orelse := {orelse := option_t.orelse _inst_1}, failure := option_t.fail _inst_1}
Equations
- option_t.lift ma = {run := option.some <$> ma}
@[instance]
Equations
- option_t.has_monad_lift = {monad_lift := option_t.lift _inst_1}
@[instance]
def
option_t.monad_functor
{m : Type u → Type v}
[monad m]
(m' : Type u → Type v)
[monad m'] :
monad_functor m m' (option_t m) (option_t m')
Equations
- option_t.monad_functor m' = {monad_map := λ (α : Type u), option_t.monad_map}
Equations
- ma.catch handle = {run := ma.run >>= λ (_p : option α), option_t.catch._match_1 handle _p}
- option_t.catch._match_1 handle (option.some a) = has_pure.pure ↑a
- option_t.catch._match_1 handle option.none = (handle ()).run
@[instance]
Equations
- option_t.monad_except = {throw := λ (_x : Type u) (_x_1 : unit), option_t.fail, catch := option_t.catch _inst_1}
@[instance]
def
option_t.monad_run
(m : Type u_1 → Type u_2)
(out : out_param (Type u_1 → Type u_2))
[monad_run out m] :
Equations
- option_t.monad_run m out = {run := λ (α : Type u_1), monad_run.run ∘ option_t.run}