mathlib3 documentation

core / init.control.option

@[protected]
def option_t.bind_cont {m : Type u Type v} [monad m] {α β : Type u} (f : α option_t m β) :
option α m (option β)
Equations
@[protected]
def option_t.bind {m : Type u Type v} [monad m] {α β : Type u} (ma : option_t m α) (f : α option_t m β) :
Equations
@[protected]
def option_t.pure {m : Type u Type v} [monad m] {α : Type u} (a : α) :
Equations
@[protected, instance]
def option_t.monad {m : Type u Type v} [monad m] :
Equations
@[protected]
def option_t.orelse {m : Type u Type v} [monad m] {α : Type u} (ma mb : option_t m α) :
Equations
@[protected]
def option_t.fail {m : Type u Type v} [monad m] {α : Type u} :
Equations
def option_t.of_option {m : Type u Type v} [monad m] {α : Type u} :
Equations
@[protected]
def option_t.lift {m : Type u Type v} [monad m] {α : Type u} (ma : m α) :
Equations
@[protected, instance]
Equations
@[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
@[protected, instance]
def option_t.monad_functor {m : Type u Type v} [monad m] (m' : Type u Type v) [monad m'] :
Equations
@[protected]
def option_t.catch {m : Type u Type v} [monad m] {α : Type u} (ma : option_t m α) (handle : unit option_t m α) :
Equations
@[protected, instance]
Equations
@[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