Function extern_spec_std_iter_Iterator_map 

pub fn extern_spec_std_iter_Iterator_map<Self_, B, F>(
    self_: Self_,
    f: F,
) -> Map<Self_, F>
where
    Self_: Sized + IteratorSpec + ?Sized + Iterator,
    F: FnMut(Self_::Item) -> B,

extern spec for ::std::iter::Iterator::map<B, F>

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

terminates

ghost

requires

forall<e, i2>
                                self.produces(Seq::singleton(e), i2) ==>
                                f.precondition((e,))

requires

map::reinitialize::<Self, B, F>()

requires

map::preservation::<Self, B, F>(self, f)

ensures

result.iter() == self && result.func() == f