Function extern_spec_std_vec_from_elem 

pub fn extern_spec_std_vec_from_elem<T: Clone>(elem: T, n: usize) -> Vec<T>

extern spec for [::std::vec::from_elem<T>]

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

ensures

result@.len() == n@

ensures

forall<i> 0 <= i && i < n@ ==> result[i] == elem