source
@[reducible, inline]
abbrev Lake.ExitCode :
Type

A process exit / return code.

Equations

- Lake.ExitCode = UInt32

Instances For

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

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

Instances

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

- Lake.instMonadExitOfMonadLift = { exit := fun {α : Type ?u.26} (rc : Lake.ExitCode) => liftM (Lake.exit rc) }

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

Equations

- Lake.exitIfErrorCode rc = if (rc != 0) = true then Lake.exit rc else pure ()

Instances For