Documentation

Lake.Util.Error

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

Type (max (u + 1) v)

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

Instances

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

Equations

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

instance Lake.instMonadErrorIO :

Equations

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

instance Lake.instMonadErrorEIOString :

MonadError (EIO String)

Equations

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

instance Lake.instMonadErrorExceptString :

MonadError (Except String)

Equations

Lake.instMonadErrorExceptString = { error := fun {α : Type ?u.7} (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