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

Equations

• Lake.instMonadError = { error := fun {α : Type u_1} (msg : String) => liftM (Lake.error msg) }

instance Lake.instMonadErrorIO : Lake.MonadError IO

Equations

• Lake.instMonadErrorIO = { error := fun {α : Type} (msg : String) => throw (IO.userError msg) }

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

Equations

• Lake.instMonadErrorEIOString = { error := fun {α : Type} (msg : String) => throw msg }

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

Equations

• Lake.instMonadErrorExceptString = { error := fun {α : Type u_1} (msg : String) => throw msg }

@[inline]

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.

Equations

• Lake.MonadError.runEIO x = do let __do_lift ← liftM (EIO.toBaseIO x) match __do_lift with | Except.ok a => pure a | Except.error e => Lake.error (toString e)

@[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.

Equations

• Lake.MonadError.runIO x = Lake.MonadError.runEIO x