Function extern_spec_FromIterator__ref_char_Box_str_from_iter 

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

extern spec for Box<str>::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.map(|c: &char| *c)