- exit : {α : Type u} → Lake.ExitCode → m α
Instances
instance
Lake.instMonadExit
{m : Type u_1 → Type u_2}
{n : Type u_1 → Type u_3}
[MonadLift m n]
[Lake.MonadExit m]
:
@[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.