feat: add `isExclusiveUnsafe`

src/Init/Util.lean

diff --git a/src/Init/Util.lean b/src/Init/Util.lean
index 0cdb92f..974eed1 100644
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@@ -45,6 +45,13 @@
 @[extern "lean_ptr_addr"]
 unsafe opaque ptrAddrUnsafe {α : Type u} (a : @& α) : USize
 
+/--
+Returns `true` if `a` is an exclusive object.
+We say an object is exclusive if it is single-threaded and its reference counter is 1.
+-/
+@[extern "lean_is_exclusive_obj"]
+unsafe opaque isExclusiveUnsafe {α : Type u} (a : @& α) : Bool
+
 set_option linter.unusedVariables.funArgs false in
 @[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
   k (ptrAddrUnsafe a)

src/include/lean/lean.h

diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 45dd5ae..e2f704a 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -481,6 +481,10 @@
     }
 }
 
+static inline uint8_t lean_is_exclusive_obj(lean_object * o) {
+    return lean_is_exclusive(o);
+}
+
 static inline bool lean_is_shared(lean_object * o) {
     if (LEAN_LIKELY(lean_is_st(o))) {
         return o->m_rc > 1;