Function lean_mk_empty_float_array

src/sarray/float.rs:5–14

(capacity: b_lean_obj_arg)

#[inline]
pub unsafe fn lean_mk_empty_float_array(capacity: b_lean_obj_arg) -> lean_obj_res {
    if !lean_is_scalar(capacity) {
        lean_internal_panic_out_of_memory()
    }
    lean_alloc_sarray(
        core::mem::size_of::<f64>() as c_uint,
        0,
        lean_unbox(capacity),
    )
}

#[inline(always)]
pub unsafe fn lean_float_array_size(a: b_lean_obj_arg) -> lean_obj_res {