Function vstd::std_specs::vec::ex_vec_insert

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