@[reducible, inline]

abbrev Lake.ExitCode : Type

A process exit / return code.

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

• exit {α : Type u} : ExitCode → m α

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

@[inline]

def Lake.exitIfErrorCode {m : Type → Type u_1} [Pure m] [MonadExit m] (rc : ExitCode) : m Unit

Exit with ExitCode if it is not 0. Otherwise, continue.