flux_core/iter/adapters/
map.rs

1use flux_attrs::*;
2
3#[extern_spec(core::iter)]
4#[refined_by(inner: I)]
5struct Map<I, F>;
6
7#[extern_spec(core::iter)]
8#[assoc(
9    fn size(x: Map<I>) -> int { <I as Iterator>::size(x.inner) }
10    fn done(x: Map<I>) -> bool { <I as Iterator>::done(x.inner) }
11    fn step(x: Map<I>, y: Map<I>) -> bool { <I as Iterator>::step(x.inner, y.inner) }
12)]
13impl<B, I: Iterator, F: FnMut(I::Item) -> B> Iterator for Map<I, F> {
14    #[spec(fn(self: &mut Self[@curr_s]) -> Option<B>[!<Self as Iterator>::done(curr_s)]
15           ensures self: Self{next_s: <Self as Iterator>::step(curr_s, next_s)})]
16    fn next(&mut self) -> Option<B>;
17}