[ base ] Add casts between Int and ExitCode (idris-lang#3432)

libs/base/System.idr

@@ -294,11 +294,20 @@ data ExitCode : Type where
   ||| @prf   Proof that the int value is non-zero.
   ExitFailure : (errNo    : Int) -> (So (not $ errNo == 0)) => ExitCode
 
+export
+Cast Int ExitCode where
+  cast 0 = ExitSuccess
+  cast code = ExitFailure code @{believe_me Oh}
+
+export
+Cast ExitCode Int where
+  cast ExitSuccess = 0
+  cast (ExitFailure code) = code
+
 ||| Exit the program normally, with the specified status.
 export
 exitWith : HasIO io => ExitCode -> io a
-exitWith ExitSuccess = primIO $ believe_me $ prim__exit 0
-exitWith (ExitFailure code) = primIO $ believe_me $ prim__exit code
+exitWith = primIO . believe_me . prim__exit . cast
 
 ||| Exit the program with status value 1, indicating failure.
 ||| If you want to specify a custom status value, see `exitWith`.