Function extern_spec_std_iter_Iterator_collect 

pub fn extern_spec_std_iter_Iterator_collect<Self_, B>(self_: Self_) -> B
where
    Self_: Sized + IteratorSpec + ?Sized + Iterator,
    B: FromIteratorSpec<Self_::Item>,

extern spec for ::std::iter::Iterator::collect<B>

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

ensures

exists<done: &mut Self, prod>
                    resolve(^done) && done.completed() && self.produces(prod, *done) && B::from_iter_post(prod, result)