pub trait IteratorSpec: Iterator {
// Required methods
spec fn obeys_prophetic_iter_laws(&self) -> bool;
spec fn remaining(&self) -> Seq<Self::Item>;
spec fn produces(&self) -> Seq<bool>;
spec fn decrease(&self) -> Option<nat>;
spec fn peek(&self, index: int) -> Option<Self::Item>;
}Required Methods§
Sourcespec fn obeys_prophetic_iter_laws(&self) -> bool
spec fn obeys_prophetic_iter_laws(&self) -> bool
This iterator obeys the specifications below on next,
expressed in terms of prophetic spec functions.
Only finite iterators (i.e., those that eventually return None
and then continue to return None) or infinite iterators that
never return None should use this interface.
Sourcespec fn produces(&self) -> Seq<bool>
spec fn produces(&self) -> Seq<bool>
For each potential item in remaining(), does the item actually
get returned, or does the iterator get “stuck” trying to produce it,
e.g., because a client supplied a closure that diverges?
Sourcespec fn decrease(&self) -> Option<nat>
spec fn decrease(&self) -> Option<nat>
Value used by default for the decreases clause when no explicit decreases clause is provided (the user can override this with an explicit decreases clause). If there’s no appropriate metric to decrease, this can return None, and the user will have to provide an explicit decreases clause.
Dyn Compatibility§
This trait is dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety".