Function extern_spec_T_FromIterator_T_Vec_T_from_iter 

pub fn extern_spec_T_FromIterator_T_Vec_T_from_iter<T, I: IntoIterator<Item = T, IntoIter: IteratorSpec>>(
    iter: I,
) -> Vec<T>

extern spec for Vec<T>::from_iter

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

requires

I::into_iter.precondition((iter,))

ensures

exists<into_iter: I::IntoIter, done: &mut I::IntoIter>
    I::into_iter.postcondition((iter,), into_iter) &&
    into_iter.produces(result@, *done) && done.completed() && resolve(^done)