Function extern_spec_T__slice_T_to_vec 

pub fn extern_spec_T__slice_T_to_vec<T>(self_: &[T]) -> Vec<T>
where
    T: Clone,

extern spec for slice<T>::to_vec

This is not a real function: its only use is for documentation.

ensures

result@.len() == self@.len()

ensures

forall<i> 0 <= i && i < self@.len() ==> <T as Clone>::clone.postcondition((&self@[i],), result@[i])