pub unsafe fn lean_string_size(o: b_lean_obj_arg) -> usize