Function lean_py_of_int64

LeanPy/native/python_bridge.c:484–494

Lean's `Int` may be a small scalar or a big integer (mpz). For now we * support the int64 range and error otherwise; this is what 99% of API * surface needs. Callers needing arbitrary precision can stringify. */

/*  Conversions: Lean → Python                                         */
/* ------------------------------------------------------------------ */

LEAN_EXPORT lean_obj_res lean_py_of_bool(uint8_t b, lean_obj_arg world) {
    (void)world; ENSURE_INIT(); WITH_GIL();
    return ok_owned_or_err(p_PyBool_FromLong(b ? 1 : 0));
}

/* Lean's `Int` may be a small scalar or a big integer (mpz). For now we
 * support the int64 range and error otherwise; this is what 99% of API
 * surface needs. Callers needing arbitrary precision can stringify. */
LEAN_EXPORT lean_obj_res lean_py_of_int64(b_lean_obj_arg n, lean_obj_arg world) {
    (void)world; ENSURE_INIT(); WITH_GIL();
    long long v;
    if (lean_is_scalar(n)) {
        v = (long long) lean_scalar_to_int64(n);