inductive System.ExitCode : Type

Exit codes for process termination.

$$\text{ExitCode} ::= \text{success} \mid \text{failure}(n : \mathbb{N}_{32})$$

• success : ExitCode

  Successful termination (code 0).

• failure : UInt32 → ExitCode

  Failure with an exit code.

def System.instBEqExitCode.beq : ExitCode → ExitCode → Bool

Equations

• System.instBEqExitCode.beq System.ExitCode.success System.ExitCode.success = true
• System.instBEqExitCode.beq (System.ExitCode.failure a) (System.ExitCode.failure b) = (a == b)
• System.instBEqExitCode.beq x✝¹ x✝ = false

@[implicit_reducible]

instance System.instBEqExitCode : BEq ExitCode

Equations

• System.instBEqExitCode = { beq := System.instBEqExitCode.beq }

def System.instReprExitCode.repr : ExitCode → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• System.instReprExitCode.repr System.ExitCode.success prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "System.ExitCode.success")).group prec✝

@[implicit_reducible]

instance System.instReprExitCode : Repr ExitCode

Equations

• System.instReprExitCode = { reprPrec := System.instReprExitCode.repr }

@[implicit_reducible]

instance System.ExitCode.instToString : ToString ExitCode

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def System.ExitCode.toUInt32 : ExitCode → UInt32

Convert an ExitCode to its numeric representation.

$$\text{toUInt32}(\text{success}) = 0, \quad \text{toUInt32}(\text{failure}(n)) = n$$

Equations

• System.ExitCode.success.toUInt32 = 0
• (System.ExitCode.failure a).toUInt32 = a

@[inline]

def System.ExitCode.isSuccess : ExitCode → Bool

Test if the exit code represents success.

$$\text{isSuccess}(\text{success}) = \text{true}$$

Equations

• System.ExitCode.success.isSuccess = true
• (System.ExitCode.failure a).isSuccess = false

theorem System.ExitCode.success_toUInt32 : success.toUInt32 = 0

Success has code 0.

theorem System.ExitCode.isSuccess_iff (c : ExitCode) : c.isSuccess = true ↔ c = success

isSuccess is true only for success.

def System.exitWith {α : Type} (code : ExitCode) : IO α

Exit the process with the given exit code.

$$\text{exitWith} : \text{ExitCode} \to \text{IO}\ \alpha$$

Note: Lean's IO.Process.exit takes UInt8, so codes above 255 are truncated.

Equations

• System.exitWith System.ExitCode.success = IO.Process.exit 0
• System.exitWith (System.ExitCode.failure a) = IO.Process.exit a.toUInt8

def System.exitSuccess {α : Type} : IO α

Exit successfully (code 0).

$$\text{exitSuccess} : \text{IO}\ \alpha$$

Equations

• System.exitSuccess = System.exitWith System.ExitCode.success

def System.exitFailure {α : Type} : IO α

Exit with failure code 1.

$$\text{exitFailure} : \text{IO}\ \alpha$$

Equations

• System.exitFailure = System.exitWith (System.ExitCode.failure 1)