Trait vstd::pervasive::ForLoopGhostIteratorNew
source · pub trait ForLoopGhostIteratorNew {
type GhostIter;
// Required method
spec fn ghost_iter(&self) -> Self::GhostIter;
}Required Associated Types§
Required Methods§
sourcespec fn ghost_iter(&self) -> Self::GhostIter
spec fn ghost_iter(&self) -> Self::GhostIter
Implementations on Foreign Types§
source§impl<A: StepSpec> ForLoopGhostIteratorNew for Range<A>
impl<A: StepSpec> ForLoopGhostIteratorNew for Range<A>
source§open spec fn ghost_iter(&self) -> RangeGhostIterator<A>
open spec fn ghost_iter(&self) -> RangeGhostIterator<A>
{
RangeGhostIterator {
start: self.start,
cur: self.start,
end: self.end,
}
}