pub unsafe fn lean_string_byte_size(o: *mut lean_object) -> usize