feat(library/init/util): add panic primitive

library/init/util.lean

@@ -23,3 +23,6 @@ f ()
 
 @[extern c inline "#4"]
 unsafe def unsafeCast {α : Type u} {β : Type v} [Inhabited β] (a : α) : β := default _
+
+@[effectful, extern c inline "lean_panic_fn(#3)"]
+constant panic {α : Type u} [Inhabited α] (msg : String) : α := default _

src/runtime/lean.h

@@ -246,6 +246,7 @@ __attribute__((noreturn)) void lean_panic(char const * msg);
 __attribute__((noreturn)) void lean_panic_out_of_memory();
 __attribute__((noreturn)) void lean_panic_unreachable();
 __attribute__((noreturn)) void lean_panic_rc_overflow();
+lean_object * lean_panic_fn(lean_object * msg);
 
 static inline size_t lean_align(size_t v, size_t a) {
     return (v / a)*a + a * (v % a != 0);

src/runtime/object.cpp

@@ -38,6 +38,10 @@ extern "C" void lean_panic_rc_overflow() {
     lean_panic("reference counter overflowed");
 }
 
+extern "C" object * lean_panic_fn(object * msg) {
+    lean_panic(lean_string_cstr(msg));
+}
+
 extern "C" size_t lean_object_byte_size(lean_object * o) {
     if (lean_is_mt(o) || lean_is_st(o) || lean_is_persistent(o)) {
         /* Recall that multi-threaded, single-threaded and persistent objects are stored in the heap.