@[inline]
def
ReaderT.orElse
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
{α : Type u_1}
[inst : Alternative m]
(x₁ : ReaderT ρ m α)
(x₂ : Unit → ReaderT ρ m α)
:
ReaderT ρ m α
Equations
- ReaderT.orElse x₁ x₂ s = HOrElse.hOrElse (x₁ s) fun x => x₂ () s
@[inline]
def
ReaderT.failure
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
{α : Type u_1}
[inst : Alternative m]
:
ReaderT ρ m α
Equations
- ReaderT.failure x = failure
instance
ReaderT.instAlternativeReaderT
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
[inst : Alternative m]
[inst : Monad m]
:
Alternative (ReaderT ρ m)
Equations
- ReaderT.instAlternativeReaderT = Alternative.mk (fun {α} => ReaderT.failure) fun {α} => ReaderT.orElse
instance
instMonadControlReaderT
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
:
MonadControl m (ReaderT ρ m)
Equations
- instMonadControlReaderT = { stM := id, liftWith := fun {α} f ctx => f fun {β} x => x ctx, restoreM := fun {α} x x_1 => x }
instance
ReaderT.tryFinally
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
[inst : MonadFinally m]
[inst : Monad m]
:
MonadFinally (ReaderT ρ m)
Equations
- ReaderT.tryFinally = { tryFinally' := fun {α β} x h ctx => tryFinally' (x ctx) fun a? => h a? ctx }