From a314981d2b06ae07d1883d8144fcab06838d45a1 Mon Sep 17 00:00:00 2001
From: Viktor Yudov <me@spcfox.com>
Date: Mon, 2 Dec 2024 15:19:28 +0300
Subject: [PATCH] [ base ] Add casts between `Int` and `ExitCode`

---
 libs/base/System.idr | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/libs/base/System.idr b/libs/base/System.idr
index b556239447..e44ee5f4c3 100644
--- a/libs/base/System.idr
+++ b/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`.