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

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

@[instance_reducible]

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

Equations

• Lake.instMonadErrorOfMonadLift = { error := fun {α : Type ?u.3} (msg : String) => liftM (Lake.error msg) }

@[instance_reducible]

instance Lake.instMonadErrorIO : MonadError IO

Equations

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

@[instance_reducible]

instance Lake.instMonadErrorEIOString : MonadError (EIO String)

Equations

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

@[instance_reducible]

instance Lake.instMonadErrorExceptString : 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} [Monad m] [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 x.toBaseIO 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] [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