Function vstd::std_specs::vec::ex_vec_append
source · pub exec fn ex_vec_append<T, A: Allocator>(
vec: &mut Vec<T, A>,
other: &mut Vec<T, A>
)
Expand description
ensures
vec@ == old(vec)@ + old(other)@,
other@ == Seq::<T>::empty(),