Function lean_py_of_lean_obj

LeanPy/native/python_bridge.c:1176–1191

* lean_py_of_lean_obj: wrap any lean_object* as a Python LeanObjHandle, * then return it as a Lean Py (external class wrapping PyObject*). * * @[extern "lean_py_of_lean_obj"] * opaque Py.ofLeanObj (obj : @& α) : IO Py */

/* ---- Lean-facing FFI ------------------------------------------------- */

/*
 * lean_py_of_lean_obj: wrap any lean_object* as a Python LeanObjHandle,
 * then return it as a Lean Py (external class wrapping PyObject*).
 *
 * @[extern "lean_py_of_lean_obj"]
 * opaque Py.ofLeanObj (obj : @& α) : IO Py
 */
LEAN_EXPORT lean_obj_res lean_py_of_lean_obj(b_lean_obj_arg obj, lean_obj_arg world) {
    (void)world;
    ENSURE_INIT(); WITH_GIL();

    PyObject *type = get_lean_obj_handle_type();
    if (!type) return raise_io_error("LeanPy: failed to create LeanObjHandle type");

    PyObject *inst = p_PyType_GenericAlloc(type, 0);
    if (!inst) return raise_py_error();

    LeanObjHandle *h = (LeanObjHandle *)inst;