Function extern_spec_core_iter_Iterator_map 

pub fn extern_spec_core_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 ::core::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) && inv(e) ==>
     f.precondition((e,))

requires

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

requires

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

ensures

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