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

Equations

• instToBoolOption = { toBool := Option.isSome }

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

Equations

• OptionT m α = m (Option α)

@[inline]

def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) : m (Option α)

Equations

• x.run = x

def OptionT.mk {m : Type u → Type v} {α : Type u} (x : m (Option α)) : OptionT m α

Equations

• OptionT.mk x = x

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[always_inline]

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

Equations

• OptionT.instMonad = Monad.mk

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

Equations

• OptionT.instAlternative = Alternative.mk (fun {α : Type u} => OptionT.fail) fun {α : Type u} => OptionT.orElse

@[inline]

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

Equations

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

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

Equations

• OptionT.instMonadLift = { monadLift := fun {α : Type u} => OptionT.lift }

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

instance OptionT.instMonadExceptOfOfMonad {m : Type u → Type v} (ε : Type u) [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m)

Equations

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

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.