Documentation

Init.Control.Reader

@[inline]
def ReaderT.orElse {m : Type u_1Type u_2} {ρ : Type u_1} {α : Type u_1} [inst : Alternative m] (x₁ : ReaderT ρ m α) (x₂ : UnitReaderT ρ m α) :
ReaderT ρ m α
Equations
@[inline]
def ReaderT.failure {m : Type u_1Type u_2} {ρ : Type u_1} {α : Type u_1} [inst : Alternative m] :
ReaderT ρ m α
Equations
instance ReaderT.instAlternativeReaderT {m : Type u_1Type u_2} {ρ : Type u_1} [inst : Alternative m] [inst : Monad m] :
Equations
  • ReaderT.instAlternativeReaderT = Alternative.mk (fun {α} => ReaderT.failure) fun {α} => ReaderT.orElse
instance instMonadControlReaderT {m : Type u_1Type u_2} {ρ : Type u_1} :
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_1Type u_2} {ρ : Type u_1} [inst : MonadFinally m] [inst : Monad m] :
Equations
  • ReaderT.tryFinally = { tryFinally' := fun {α β} x h ctx => tryFinally' (x ctx) fun a? => h a? ctx }
noncomputable def Reader (ρ : Type u) (α : Type u) :
Type u
Equations