Function vstd::std_specs::vec::ex_vec_clone

source · 
pub exec fn ex_vec_clone<T: Clone, A: Allocator + Clone>(
    vec: &Vec<T, A>
) -> Vec<T, A>
Expand description
ensures
res.len() == vec.len(),
forall |i| 0 <= i < vec.len() ==> call_ensures(T::clone, (&vec[i],), res[i]),
vec_clone_trigger(*vec, res),
vec@ =~= res@ ==> vec@ == res@,