pub unsafe fn lean_float_array_size(a: b_lean_obj_arg) -> lean_obj_res