Function extern_spec_FromIterator__ref_str_String_from_iter 

pub fn extern_spec_FromIterator__ref_str_String_from_iter<'a, I: IntoIterator<Item = &'a str, IntoIter: IteratorSpec>>(
    iter: I,
) -> String

extern spec for String::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, produced: Seq<I::Item>, done: &mut I::IntoIter>
    I::into_iter.postcondition((iter,), into_iter) &&
    into_iter.produces(produced, *done) && done.completed() && resolve(^done) &&
    result@ == produced.flat_map(|s: I::Item| s@)