mathlib documentation

core / init.control.option

structure option_t (m : Type uType v) (α : Type u) :
Type v
@[protected]
def option_t.bind_cont {m : Type uType v} [monad m] {α β : Type u} (f : α → option_t m β) :
option αm (option β)
Equations
@[protected]
def option_t.bind {m : Type uType v} [monad m] {α β : Type u} (ma : option_t m α) (f : α → option_t m β) :
Equations
@[protected]
def option_t.pure {m : Type uType v} [monad m] {α : Type u} (a : α) :
Equations
@[protected, instance]
def option_t.monad {m : Type uType v} [monad m] :
Equations
@[protected]
def option_t.orelse {m : Type uType v} [monad m] {α : Type u} (ma mb : option_t m α) :
Equations
@[protected]
def option_t.fail {m : Type uType v} [monad m] {α : Type u} :
Equations
def option_t.of_option {m : Type uType v} [monad m] {α : Type u} :
option αoption_t m α
Equations
@[protected, instance]
def option_t.alternative {m : Type uType v} [monad m] :
Equations
@[protected]
def option_t.lift {m : Type uType v} [monad m] {α : Type u} (ma : m α) :
Equations
@[protected, instance]
def option_t.has_monad_lift {m : Type uType v} [monad m] :
Equations
@[protected]
def option_t.monad_map {m : Type uType v} [monad m] {m' : Type uType u_1} [monad m'] {α : Type u} (f : Π {α : Type u}, m αm' α) :
option_t m αoption_t m' α
Equations
@[protected, instance]
def option_t.monad_functor {m : Type uType v} [monad m] (m' : Type uType v) [monad m'] :
Equations
@[protected]
def option_t.catch {m : Type uType v} [monad m] {α : Type u} (ma : option_t m α) (handle : unitoption_t m α) :
Equations
@[protected, instance]
def option_t.monad_except {m : Type uType v} [monad m] :
Equations
@[protected, instance]
def option_t.monad_run (m : Type u_1Type u_2) (out : out_param (Type u_1Type u_2)) [monad_run out m] :
monad_run (λ (α : Type u_1), out (option α)) (option_t m)
Equations