Documentation

Lake.Util.Error

class Lake.MonadError (m : Type u → Type v) :
Type (max (u + 1) v)
Instances
    instance Lake.instMonadErrorOfMonadLift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLift m n] [Lake.MonadError m] :
    Equations
    Equations
    @[inline]
    def Lake.MonadError.runEIO {m : TypeType u_1} {ε : Type} {α : Type} [Monad m] [Lake.MonadError m] [MonadLiftT BaseIO m] [ToString ε] (x : EIO ε α) :
    m α

    Perform an EIO action. If it throws an error, invoke error with its string representation.

    Equations
    Instances For
      @[inline]
      def Lake.MonadError.runIO {m : TypeType u_1} {α : Type} [Monad m] [Lake.MonadError m] [MonadLiftT BaseIO m] (x : IO α) :
      m α

      Perform an IO action. If it throws an error, invoke error with its string representation.

      Equations
      Instances For