mathlib documentation

core.init.control.option

structure option_t  :
(Type uType v)Type uType v

def option_t.bind_cont {m : Type uType v} [monad m] {α β : Type u} :
(α → option_t m β)option αm (option β)

Equations
def option_t.bind {m : Type uType v} [monad m] {α β : Type u} :
option_t m α(α → option_t m β)option_t m β

Equations
def option_t.pure {m : Type uType v} [monad m] {α : Type u} :
α → option_t m α

Equations
@[instance]
def option_t.monad {m : Type uType v} [monad m] :

Equations
def option_t.orelse {m : Type uType v} [monad m] {α : Type u} :
option_t m αoption_t m αoption_t m α

Equations
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
def option_t.lift {m : Type uType v} [monad m] {α : Type u} :
m αoption_t m α

Equations
@[instance]
def option_t.has_monad_lift {m : Type uType v} [monad m] :

Equations
def option_t.monad_map {m : Type uType v} [monad m] {m' : Type uType u_1} [monad m'] {α : Type u} :
(Π {α : Type u}, m αm' α)option_t m αoption_t m' α

Equations
@[instance]
def option_t.monad_functor {m : Type uType v} [monad m] (m' : Type uType v) [monad m'] :

Equations
def option_t.catch {m : Type uType v} [monad m] {α : Type u} :
option_t m α(unitoption_t m α)option_t m α

Equations
@[instance]
def option_t.monad_except {m : Type uType v} [monad m] :

Equations
@[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