pub trait ForLoopGhostIterator {
type ExecIter;
type Item;
type Decrease;
// Required methods
spec fn exec_invariant(&self, exec_iter: &Self::ExecIter) -> bool;
spec fn ghost_invariant(&self, init: Option<&Self>) -> bool;
spec fn ghost_ensures(&self) -> bool;
spec fn ghost_decrease(&self) -> Option<Self::Decrease>;
spec fn ghost_peek_next(&self) -> Option<Self::Item>;
spec fn ghost_advance(&self, exec_iter: &Self::ExecIter) -> Self
where Self: Sized;
}Required Associated Types§
Required Methods§
Sourcespec fn exec_invariant(&self, exec_iter: &Self::ExecIter) -> bool
spec fn exec_invariant(&self, exec_iter: &Self::ExecIter) -> bool
Sourcespec fn ghost_invariant(&self, init: Option<&Self>) -> bool
spec fn ghost_invariant(&self, init: Option<&Self>) -> bool
Sourcespec fn ghost_ensures(&self) -> bool
spec fn ghost_ensures(&self) -> bool
Sourcespec fn ghost_decrease(&self) -> Option<Self::Decrease>
spec fn ghost_decrease(&self) -> Option<Self::Decrease>
Sourcespec fn ghost_peek_next(&self) -> Option<Self::Item>
spec fn ghost_peek_next(&self) -> Option<Self::Item>
Sourcespec fn ghost_advance(&self, exec_iter: &Self::ExecIter) -> Selfwhere
Self: Sized,
spec fn ghost_advance(&self, exec_iter: &Self::ExecIter) -> Selfwhere
Self: Sized,
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.