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(),