pub fn extern_spec_alloc_vec_T_Vec_T_new<T>() -> Vec<T>Expand description
extern spec for ::alloc::vec::Vec<T>::new
This is not a real function: its only use is for documentation.
terminates
ghost
ensures
result@.len() == 0pub fn extern_spec_alloc_vec_T_Vec_T_new<T>() -> Vec<T>extern spec for ::alloc::vec::Vec<T>::new
This is not a real function: its only use is for documentation.
terminates
ghost
ensures
result@.len() == 0