Documentation

Init.Control.Reader

@[inline]
def ReaderT.orElse {m : Type u_1 → Type u_2} {ρ : Type u_1} {α : Type u_1} [Alternative m] (x₁ : ReaderT ρ m α) (x₂ : UnitReaderT ρ m α) :
ReaderT ρ m α
Equations
Instances For
    @[inline]
    def ReaderT.failure {m : Type u_1 → Type u_2} {ρ : Type u_1} {α : Type u_1} [Alternative m] :
    ReaderT ρ m α
    Equations
    Instances For
      instance ReaderT.instAlternativeOfMonad {m : Type u_1 → Type u_2} {ρ : Type u_1} [Alternative m] [Monad m] :
      Equations
      • ReaderT.instAlternativeOfMonad = Alternative.mk (fun {α : Type ?u.30} => ReaderT.failure) fun {α : Type ?u.30} => ReaderT.orElse
      instance instMonadControlReaderT {m : Type u_1 → Type u_2} {ρ : Type u_1} :
      Equations
      • One or more equations did not get rendered due to their size.
      @[always_inline]
      instance ReaderT.tryFinally {m : Type u_1 → Type u_2} {ρ : Type u_1} [MonadFinally m] :
      Equations
      @[reducible]
      def ReaderM (ρ : Type u) (α : Type u) :
      Equations
      Instances For