Function lean_mk_empty_array_with_capacity

src/array/high_level.rs:22–27

(capacity: b_lean_obj_arg)

#[inline(always)]
pub unsafe fn lean_mk_empty_array_with_capacity(capacity: b_lean_obj_arg) -> *mut lean_object {
    if !lean_is_scalar(capacity) {
        lean_internal_panic_out_of_memory()
    }
    lean_alloc_array(0, lean_unbox(capacity))
}

#[inline]
pub unsafe fn lean_array_uget(a: b_lean_obj_arg, i: usize) -> lean_obj_res {