Function vstd::std_specs::vec::ex_vec_remove

source · 
pub exec fn ex_vec_remove<T, A: Allocator>(vec: &mut Vec<T, A>, i: usize) -> element : T
Expand description
requires
i < old(vec).len(),
ensures
element == old(vec)[i as int],
vec@ == old(vec)@.remove(i as int),