Function vstd::std_specs::vec::ex_vec_new

source · 
pub exec fn ex_vec_new<T>() -> v : Vec<T>
Expand description
ensures
v@ == Seq::<T>::empty(),