class Lake.MonadError (m : Type u → Type v) : Type (max (u + 1) v)

• error : {α : Type u} → String → m α

instance Lake.instMonadError {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLift m n] [Lake.MonadError m] : Lake.MonadError n

instance Lake.instMonadErrorIO : Lake.MonadError IO

instance Lake.instMonadErrorEIOString : Lake.MonadError (EIO String)

instance Lake.instMonadErrorExceptString : Lake.MonadError (Except String)

def Lake.MonadError.runEIO {m : Type → Type 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.

@[inline]

def Lake.MonadError.runIO {m : Type → Type 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.