flux_core/iter/adapters/
skip.rs

1use flux_attrs::*;
2
3#[extern_spec(core::iter)]
4#[refined_by(size: int)]
5struct Skip<I>;
6
7// TODO: See discussion here: https://github.com/flux-rs/flux/pull/1170#discussion_r2198219054
8// We should store the number of skipped elements in the refined_by and compute the size
9// based on the inner iterator here, but you can’t quite do that because that requires
10// “stepping” the inner iterator N times (when you construct the Skip). We could possibly generalize
11// the `step` to take an `int` count ...
12
13#[extern_spec(core::iter)]
14#[assoc(
15    fn size(r: Skip) -> int { r.size }
16    fn step(self: Skip, other: Skip) -> bool { other.size == self.size - 1 }
17)]
18impl<I: Iterator> Iterator for Skip<I> {
19    #[spec(
20        fn(self: &mut Self[@curr_s]) -> Option<_>[!<Self as Iterator>::done(curr_s)]
21        ensures self: Self{next_s: <Self as Iterator>::step(curr_s, next_s)}
22    )]
23    fn next(&mut self) -> Option<I::Item>;
24}
flux_core/iter/adapters/skip.rs

flux_core/iter/adapters/
skip.rs
