pub unsafe fn lean_string_utf8_byte_size(s: b_lean_obj_arg) -> lean_obj_res