mathlib docs: core.init.control.option

ma.orelse mb = {run := ma.run >>= λ (_p : option α), option_t.orelse._match_1 mb _p}
option_t.orelse._match_1 mb (some a) = pure (some a)
option_t.orelse._match_1 mb none = mb.run

source

def option_t.fail {m : Type u → Type v} [monad m] {α : Type u} :

option_t m α

Equations

option_t.fail = {run := pure none}

source

def option_t.of_option {m : Type u → Type v} [monad m] {α : Type u} (a : option α) :

option_t m α

Equations

option_t.of_option o = {run := pure o}

source

@[instance]

def option_t.alternative {m : Type u → Type v} [monad m] :

alternative (option_t m)

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}

source

def option_t.lift {m : Type u → Type v} [monad m] {α : Type u} (ma : m α) :

option_t m α

Equations

option_t.lift ma = {run := some <$> ma}

source

@[instance]

def option_t.has_monad_lift {m : Type u → Type v} [monad m] :

has_monad_lift m (option_t m)

Equations

option_t.has_monad_lift = {monad_lift := option_t.lift _inst_1}

source

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' α) (a : option_t m α) :

option_t m' α

Equations

option_t.monad_map f = λ (x : option_t m α), {run := f x.run}

source

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

source

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

ma.catch handle = {run := ma.run >>= λ (_p : option α), option_t.catch._match_1 handle _p}
option_t.catch._match_1 handle (some a) = pure ↑a
option_t.catch._match_1 handle none = (handle ()).run

source

@[instance]

def option_t.monad_except {m : Type u → Type v} [monad m] :

monad_except unit (option_t m)

Equations

option_t.monad_except = {throw := λ (_x : Type u) (_x_1 : unit), option_t.fail, catch := option_t.catch _inst_1}

source

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

option_t.monad_run m out = {run := λ (α : Type u_1), run ∘ option_t.run}