Trait vstd::pervasive::ForLoopGhostIterator
source · pub trait ForLoopGhostIterator {
type ExecIter;
type Item;
type Decrease;
// Required methods
fn exec_invariant(&self, exec_iter: &Self::ExecIter) -> bool;
fn ghost_invariant(&self, init: Option<&Self>) -> bool;
fn ghost_ensures(&self) -> bool;
fn ghost_decrease(&self) -> Option<Self::Decrease>;
fn ghost_peek_next(&self) -> Option<Self::Item>;
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,
Object Safety§
This trait is not object safe.