Function extern_spec_core_iter_Iterator_collect 

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

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

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

requires

B::from_iter.precondition((self,))

ensures

B::from_iter.postcondition((self,), result)