Documentation

Lake.Util.Exit

@[inline, reducible]

A process exit / return code.

Equations
Instances For
    class Lake.MonadExit (m : Type u → Type v) :
    Type (max (u + 1) v)
    Instances
      instance Lake.instMonadExit {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLift m n] [Lake.MonadExit m] :
      Equations
      @[inline]
      def Lake.exitIfErrorCode {m : TypeType u_1} [Pure m] [Lake.MonadExit m] (rc : Lake.ExitCode) :

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

      Equations
      Instances For