Equations
- Option.instDecidableEq = Option.decEqOption✝
Lifts an optional value to any Alternative
, sending none
to failure
.
Instances For
@[deprecated Option.getM]
def
Option.toMonad
{m : Type u_1 → Type u_2}
{α : Type u_1}
[Monad m]
[Alternative m]
:
Option α → m α
Equations
- Option.toMonad = Option.getM
Instances For
@[inline]
def
Option.bindM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(f : α → m (Option β))
(o : Option α)
:
m (Option β)
Runs f
on o
's value, if any, and returns its result, or else returns none
.
Equations
- Option.bindM f o = match o with | some a => do let __do_lift ← f a pure __do_lift | x => pure none
Instances For
@[simp]
@[simp]
theorem
Option.map_some'
{α : Type u_1}
{β : Type u_2}
(a : α)
(f : α → β)
:
Option.map f (some a) = some (f a)
@[inline]
An elimination principle for Option
. It is a nondependent version of Option.recOn
.
Instances For
Lifts a relation α → β → Prop
to a relation Option α → Option β → Prop
by just adding
none ~ none
.
- some: ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : α} {b : β}, r a b → Option.Rel r (some a) (some b)
- none: ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, Option.Rel r none none
Instances For
@[inline]
def
Option.mapA
{m : Type u_1 → Type u_2}
[Applicative m]
{α : Type u_3}
{β : Type u_1}
(f : α → m β)
:
Like Option.mapM
but for applicative functors.
Equations
- Option.mapA f x = match x with | none => pure none | some x => some <$> f x
Instances For
@[inline]
If you maybe have a monadic computation in a [Monad m]
which produces a term of type α
, then
there is a naturally associated way to always perform a computation in m
which maybe produces a
result.
Instances For
@[inline]
def
Option.elimM
{m : Type u_1 → Type u_2}
{α : Type u_1}
{β : Type u_1}
[Monad m]
(x : m (Option α))
(y : m β)
(z : α → m β)
:
m β
A monadic analogue of Option.elim
.
Equations
- Option.elimM x y z = do let __do_lift ← x __do_lift.elim y z
Instances For
@[simp]
@[always_inline]
Equations
- instFunctorOption = { map := fun {α β : Type u_1} => Option.map, mapConst := fun {α β : Type u_1} => Option.map ∘ Function.const β }
@[always_inline]
Equations
- instAlternativeOption = Alternative.mk (fun {α : Type u_1} => none) fun {α : Type u_1} => Option.orElse
Equations
- liftOption x = match x with | some a => pure a | none => failure
Instances For
Equations
- instMonadExceptOfUnitOption = { throw := fun {α : Type u_1} (x : Unit) => none, tryCatch := fun {α : Type u_1} => Option.tryCatch }