Documentation

Init.Control.Option

instance instToBoolOption {α : Type u_1} :
Equations
  • instToBoolOption = { toBool := Option.toBool }
noncomputable def OptionT (m : Type uType v) (α : Type u) :
Type v
Equations
@[inline]
def OptionT.run {m : Type uType v} {α : Type u} (x : OptionT m α) :
m (Option α)
Equations
def OptionT.mk {m : Type uType v} {α : Type u} (x : m (Option α)) :
OptionT m α
Equations
@[inline]
def OptionT.bind {m : Type uType v} [inst : Monad m] {α : Type u} {β : Type u} (x : OptionT m α) (f : αOptionT m β) :
OptionT m β
Equations
@[inline]
def OptionT.pure {m : Type uType v} [inst : Monad m] {α : Type u} (a : α) :
OptionT m α
Equations
instance OptionT.instMonadOptionT {m : Type uType v} [inst : Monad m] :
Equations
  • OptionT.instMonadOptionT = Monad.mk
@[inline]
def OptionT.orElse {m : Type uType v} [inst : Monad m] {α : Type u} (x : OptionT m α) (y : UnitOptionT m α) :
OptionT m α
Equations
@[inline]
def OptionT.fail {m : Type uType v} [inst : Monad m] {α : Type u} :
OptionT m α
Equations
instance OptionT.instAlternativeOptionT {m : Type uType v} [inst : Monad m] :
Equations
  • OptionT.instAlternativeOptionT = Alternative.mk (fun {α} => OptionT.fail) fun {α} => OptionT.orElse
@[inline]
def OptionT.lift {m : Type uType v} [inst : Monad m] {α : Type u} (x : m α) :
OptionT m α
Equations
instance OptionT.instMonadLiftOptionT {m : Type uType v} [inst : Monad m] :
Equations
  • OptionT.instMonadLiftOptionT = { monadLift := fun {α} => OptionT.lift }
instance OptionT.instMonadFunctorOptionT {m : Type uType v} :
Equations
  • OptionT.instMonadFunctorOptionT = { monadMap := fun {α} f x => f (Option α) x }
@[inline]
def OptionT.tryCatch {m : Type uType v} [inst : Monad m] {α : Type u} (x : OptionT m α) (handle : UnitOptionT m α) :
OptionT m α
Equations
instance OptionT.instMonadExceptOfUnitOptionT {m : Type uType v} [inst : Monad m] :
Equations
  • OptionT.instMonadExceptOfUnitOptionT = { throw := fun {α} x => OptionT.fail, tryCatch := fun {α} => OptionT.tryCatch }
instance OptionT.instMonadExceptOfOptionT {m : Type uType v} (ε : Type u) [inst : Monad m] [inst : MonadExceptOf ε m] :
Equations
instance instMonadControlOptionT {m : Type u_1Type u_2} [inst : Monad m] :
Equations
  • instMonadControlOptionT = { stM := Option, liftWith := fun {α} f => liftM (f fun {β} x => OptionT.run x), restoreM := fun {α} x => x }