source
instance instToBoolOption {α : Type u_1} :
ToBool (Option α)
Equations

- instToBoolOption = { toBool := Option.isSome }

source
def OptionT (m : Type u → Type v) (α : Type u) :
Type v

Adds the ability to fail to a monad. Unlike ordinary exceptions, there is no way to signal why a failure occurred.

Equations

- OptionT m α = m (Option α)

Instances For

source
@[inline]
def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) :
m (Option α)

Executes an action that might fail in the underlying monad `m`, returning `none` in case of failure.

Equations

- x.run = x

Instances For

source
@[inline]
def OptionT.mk {m : Type u → Type v} {α : Type u} (x : m (Option α)) :
OptionT m α

Converts an action that returns an `Option` into one that might fail, with `none` indicating failure.

Equations

- OptionT.mk x = x

Instances For

source
@[inline]
def OptionT.bind {m : Type u → Type v} [Monad m] {α β : Type u} (x : OptionT m α) (f : α → OptionT m β) :
OptionT m β

Sequences two potentially-failing actions. The second action is run only if the first succeeds.

Equations

- x.bind f = OptionT.mk do let __do_lift ← x match __do_lift with | some a => f a | none => pure none

Instances For

source
@[inline]
def OptionT.pure {m : Type u → Type v} [Monad m] {α : Type u} (a : α) :
OptionT m α

Succeeds with the provided value.

Equations

- OptionT.pure a = OptionT.mk (pure (some a))

Instances For

source
@[always_inline]
instance OptionT.instMonad {m : Type u → Type v} [Monad m] :
Monad (OptionT m)
Equations

- One or more equations did not get rendered due to their size.

source
instance OptionT.instInhabitedOfPure {α : Type u} {m : Type u → Type v} [Pure m] :
Inhabited (OptionT m α)
Equations

- OptionT.instInhabitedOfPure = { default := pure default }

source
@[inline]
def OptionT.orElse {m : Type u → Type v} [Monad m] {α : Type u} (x : OptionT m α) (y : Unit → OptionT m α) :
OptionT m α

Recovers from failures. Typically used via the `<|>` operator.

Equations

- x.orElse y = OptionT.mk do let __do_lift ← x match __do_lift with | some a => pure (some a) | x => y ()

Instances For

source
@[inline]
def OptionT.fail {m : Type u → Type v} [Monad m] {α : Type u} :
OptionT m α

A recoverable failure.

Equations

- OptionT.fail = OptionT.mk (pure none)

Instances For

source
instance OptionT.instAlternative {m : Type u → Type v} [Monad m] :
Alternative (OptionT m)
Equations

- OptionT.instAlternative = { toApplicative := OptionT.instMonad.toApplicative, failure := fun {α : Type ?u.15} => OptionT.fail, orElse := fun {α : Type ?u.15} => OptionT.orElse }

source
@[inline]
def OptionT.lift {m : Type u → Type v} [Monad m] {α : Type u} (x : m α) :
OptionT m α

Converts a computation from the underlying monad into one that could fail, even though it does not.

This function is typically implicitly accessed via a `MonadLiftT` instance as part of automatic lifting.

Equations

- OptionT.lift x = OptionT.mk do let __do_lift ← x pure (some __do_lift)

Instances For

source
instance OptionT.instMonadLift {m : Type u → Type v} [Monad m] :
MonadLift m (OptionT m)
Equations

- OptionT.instMonadLift = { monadLift := fun {α : Type ?u.14} => OptionT.lift }

source
instance OptionT.instMonadFunctor {m : Type u → Type v} :
MonadFunctor m (OptionT m)
Equations

- OptionT.instMonadFunctor = { monadMap := fun {α : Type ?u.14} (f : {β : Type ?u.14} → m β → m β) (x : OptionT m α) => f x }

source
@[inline]
def OptionT.tryCatch {m : Type u → Type v} [Monad m] {α : Type u} (x : OptionT m α) (handle : Unit → OptionT m α) :
OptionT m α

Handles failures by treating them as exceptions of type `Unit`.

Equations

- x.tryCatch handle = OptionT.mk do let __discr ← x match __discr with | some a => pure (some a) | x => handle ()

Instances For

source
instance OptionT.instMonadExceptOfUnit {m : Type u → Type v} [Monad m] :
MonadExceptOf Unit (OptionT m)
Equations

- OptionT.instMonadExceptOfUnit = { throw := fun {α : Type ?u.16} (x : Unit) => OptionT.fail, tryCatch := fun {α : Type ?u.16} => OptionT.tryCatch }

source
instance OptionT.instMonadExceptOf {m : Type u → Type v} (ε : Type u) [MonadExceptOf ε m] :
MonadExceptOf ε (OptionT m)
Equations

- One or more equations did not get rendered due to their size.

source
instance instMonadControlOptionTOfMonad {m : Type u_1 → Type u_2} [Monad m] :
MonadControl m (OptionT m)
Equations

- One or more equations did not get rendered due to their size.