Function lean_py_of_list

LeanPy/native/python_bridge.c:515–527

    size_t n = lean_string_size(s) - 1; /* size includes terminating NUL */
    return ok_owned_or_err(p_PyUnicode_DecodeUTF8(cs, (Py_ssize_t)n, NULL));
}

LEAN_EXPORT lean_obj_res lean_py_of_bytes(b_lean_obj_arg ba, lean_obj_arg world) {
    (void)world; ENSURE_INIT(); WITH_GIL();
    Py_ssize_t n = (Py_ssize_t) lean_sarray_size(ba);
    const char *p = (const char *) lean_sarray_cptr(ba);
    return ok_owned_or_err(p_PyBytes_FromStringAndSize(p, n));
}

LEAN_EXPORT lean_obj_res lean_py_of_list(b_lean_obj_arg arr, lean_obj_arg world) {
    (void)world; ENSURE_INIT(); WITH_GIL();
    size_t n = lean_array_size(arr);
    PyObject *list = p_PyList_New((Py_ssize_t)n);
    if (!list) return raise_py_error();
    for (size_t i = 0; i < n; i++) {
        lean_object *elem = lean_array_get_core(arr, i);