diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 1f535a64c1..f0855529cb 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -445,6 +445,8 @@ def run (args : SpawnArgs) : IO String := do
     throw <| IO.userError <| "process '" ++ args.cmd ++ "' exited with code " ++ toString out.exitCode
   pure out.stdout
 
+@[extern "lean_io_exit"] constant exit : UInt8 → IO α
+
 end Process
 
 structure AccessRight where
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 9d4c96f653..8f8cecbe5e 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -837,6 +837,10 @@ extern "C" obj_res lean_io_wait_any(b_obj_arg task_list, obj_arg) {
     return io_result_mk_ok(v);
 }
 
+extern "C" obj_res lean_io_exit(obj_arg obj, obj_arg /* w */) {
+    exit((size_t) obj);
+}
+
 void initialize_io() {
     g_io_error_nullptr_read = mk_io_user_error(mk_string("null reference read"));
     mark_persistent(g_io_error_nullptr_read);