flux_core/iter/adapters/
enumerate.rs

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