Function lean_mk_empty_byte_array

src/sarray/byte.rs:5–10

(capacity: b_lean_obj_arg)

#[inline]
pub unsafe fn lean_mk_empty_byte_array(capacity: b_lean_obj_arg) -> lean_obj_res {
    if !lean_is_scalar(capacity) {
        lean_internal_panic_out_of_memory()
    }
    lean_alloc_sarray(1, 0, lean_unbox(capacity))
}

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