Function vstd::std_specs::vec::ex_vec_truncate
source · pub exec fn ex_vec_truncate<T, A: Allocator>(vec: &mut Vec<T, A>, len: usize)Expand description
ensures
len <= vec.len() ==> vec@ == old(vec)@.subrange(0, len as int),len > vec.len() ==> vec@ == old(vec)@,