Documentation

Init.Control.Reader

@[inline]
def ReaderT.orElse {m : Type u_1 → Type u_2} {ρ α : Type u_1} [Alternative m] (x₁ : ReaderT ρ m α) (x₂ : UnitReaderT ρ m α) :
ReaderT ρ m α

Recovers from errors. The same local value is provided to both branches. Typically used via the <|> operator.

Equations
    Instances For
      @[inline]
      def ReaderT.failure {m : Type u_1 → Type u_2} {ρ α : Type u_1} [Alternative m] :
      ReaderT ρ m α

      Fails with a recoverable error.

      Equations
        Instances For
          instance ReaderT.instAlternativeOfMonad {m : Type u_1 → Type u_2} {ρ : Type u_1} [Alternative m] [Monad m] :
          Equations
            instance instMonadControlReaderT {m : Type u_1 → Type u_2} {ρ : Type u_1} :
            Equations
              @[always_inline]
              instance ReaderT.tryFinally {m : Type u_1 → Type u_2} {ρ : Type u_1} [MonadFinally m] :
              Equations
                @[reducible]
                def ReaderM (ρ α : Type u) :

                A monad with access to a read-only value of type ρ. The value can be locally overridden by withReader, but it cannot be mutated.

                Equations
                  Instances For