feat: of_nat/of_int

leanprover · Dec 16, 2024 · ea15ca7 · ea15ca7
1 parent 4a08e12
commit ea15ca7
Showing 1 changed file with 32 additions and 16 deletions.
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
@@ -1183,6 +1183,24 @@ static inline lean_object * lean_set_external_data(lean_object * o, void * data)
     }
 }
 
+/* Integer scalars */
+
+static inline int64_t lean_scalar_to_int64(b_lean_obj_arg a) {
+    assert(lean_is_scalar(a));
+    if (sizeof(void*) == 8)
+        return (int)((unsigned)lean_unbox(a)); /* NOLINT */
+    else
+        return ((int)((size_t)a)) >> 1; /* NOLINT */
+}
+
+static inline int lean_scalar_to_int(b_lean_obj_arg a) {
+    assert(lean_is_scalar(a));
+    if (sizeof(void*) == 8)
+        return (int)((unsigned)lean_unbox(a)); /* NOLINT */
+    else
+        return ((int)((size_t)a)) >> 1; /* NOLINT */
+}
+
 /* Big numbers */
 
 LEAN_EXPORT lean_obj_res lean_mpz_of_usize(size_t a);
@@ -1196,6 +1214,20 @@ LEAN_EXPORT lean_obj_res lean_mpz_of_signed(int a);
 LEAN_EXPORT lean_obj_res lean_mpz_to_nat(lean_obj_arg a);
 LEAN_EXPORT lean_obj_res lean_mpz_to_int(lean_obj_arg a);
 
+static inline lean_obj_res lean_mpz_of_nat(lean_obj_arg a) {
+    if (lean_is_scalar(a))
+        return lean_mpz_of_usize(lean_unbox(a));
+    else
+        return a;
+}
+
+static inline lean_obj_res lean_mpz_of_int(lean_obj_arg a) {
+    if (lean_is_scalar(a))
+        return lean_mpz_of_signed(lean_scalar_to_int(a));
+    else
+        return a;
+}
+
 LEAN_EXPORT bool lean_mpz_eq(b_lean_obj_arg a1, b_lean_obj_arg a2);
 LEAN_EXPORT bool lean_mpz_le(b_lean_obj_arg a1, b_lean_obj_arg a2);
 LEAN_EXPORT bool lean_mpz_lt(b_lean_obj_arg a1, b_lean_obj_arg a2);
@@ -1450,22 +1482,6 @@ static inline lean_obj_res lean_int64_to_int(int64_t n) {
         return lean_big_int64_to_int(n);
 }
 
-static inline int64_t lean_scalar_to_int64(b_lean_obj_arg a) {
-    assert(lean_is_scalar(a));
-    if (sizeof(void*) == 8)
-        return (int)((unsigned)lean_unbox(a)); /* NOLINT */
-    else
-        return ((int)((size_t)a)) >> 1; /* NOLINT */
-}
-
-static inline int lean_scalar_to_int(b_lean_obj_arg a) {
-    assert(lean_is_scalar(a));
-    if (sizeof(void*) == 8)
-        return (int)((unsigned)lean_unbox(a)); /* NOLINT */
-    else
-        return ((int)((size_t)a)) >> 1; /* NOLINT */
-}
-
 static inline lean_obj_res lean_nat_to_int(lean_obj_arg a) {
     if (lean_is_scalar(a)) {
         size_t v = lean_unbox(a);