@[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} → Lake.ExitCode → m α

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

Equations

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

@[inline]

def Lake.exitIfErrorCode {m : Type → Type u_1} [Pure m] [Lake.MonadExit m] (rc : Lake.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 ()