mathlib3 documentation

core / init.control.option

source
structure option_t (m : Type u → Type v) (α : Type u) :
Type v
Instances for option_t
source
@[protected]
def option_t.bind_cont {m : Type u → Type v} [monad m] {α β : Type u} (f : α → option_t m β) :
option α → m (option β)
Equations
source
@[protected]
def option_t.bind {m : Type u → Type v} [monad m] {α β : Type u} (ma : option_t m α) (f : α → option_t m β) :
option_t m β
Equations
source
@[protected]
def option_t.pure {m : Type u → Type v} [monad m] {α : Type u} (a : α) :
option_t m α
Equations
source
@[protected, instance]
def option_t.monad {m : Type u → Type v} [monad m] :
monad (option_t m)
Equations
source
@[protected]
def option_t.orelse {m : Type u → Type v} [monad m] {α : Type u} (ma mb : option_t m α) :
option_t m α
Equations
source
@[protected]
def option_t.fail {m : Type u → Type v} [monad m] {α : Type u} :
option_t m α
Equations
source
def option_t.of_option {m : Type u → Type v} [monad m] {α : Type u} :
option α → option_t m α
Equations
source
@[protected, instance]
def option_t.alternative {m : Type u → Type v} [monad m] :
alternative (option_t m)
Equations
source
@[protected]
def option_t.lift {m : Type u → Type v} [monad m] {α : Type u} (ma : m α) :
option_t m α
Equations
source
@[protected, instance]
def option_t.has_monad_lift {m : Type u → Type v} [monad m] :
has_monad_lift m (option_t m)
Equations
source
@[protected]
def option_t.monad_map {m : Type u → Type v} [monad m] {m' : Type u → Type u_1} [monad m'] {α : Type u} (f : Π {α : Type u}, m α → m' α) :
option_t m α → option_t m' α
Equations
source
@[protected, 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
source
@[protected]
def option_t.catch {m : Type u → Type v} [monad m] {α : Type u} (ma : option_t m α) (handle : unit → option_t m α) :
option_t m α
Equations
source
@[protected, instance]
def option_t.monad_except {m : Type u → Type v} [monad m] :
monad_except unit (option_t m)
Equations
source
@[protected, 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] :
monad_run (λ (α : Type u_1), out (option α)) (option_t m)
Equations