Function extern_spec_core_iter_Iterator_map 

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

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

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

ghost

requires

self

requires

Self

requires

Self

ensures

self