Function vstd::std_specs::vec::ex_vec_split_off

source · 
pub exec fn ex_vec_split_off<T, A: Allocator + Clone>(
    vec: &mut Vec<T, A>,
    at: usize
) -> return_value : Vec<T, A>
Expand description
requires
at <= old(vec)@.len(),
ensures
vec@ == old(vec)@.subrange(0, at as int),
return_value@ == old(vec)@.subrange(at as int, old(vec)@.len() as int),