Function vstd::std_specs::vec::ex_vec_clone

pub exec fn ex_vec_clone<T: Clone, A: Allocator + Clone>(
    vec: &Vec<T, A>
) -> res : 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@,