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, Key> ForLoopGhostIteratorNew for Iter<'a, Key>
impl<'a, Key> ForLoopGhostIteratorNew for Iter<'a, Key>
source§open spec fn ghost_iter(&self) -> IterGhostIterator<'a, Key>
open spec fn ghost_iter(&self) -> IterGhostIterator<'a, Key>
{
IterGhostIterator {
pos: self@.0,
elements: self@.1,
phantom: None,
}
}type GhostIter = IterGhostIterator<'a, Key>
source§impl<'a, Key, Value> ForLoopGhostIteratorNew for Keys<'a, Key, Value>
impl<'a, Key, Value> ForLoopGhostIteratorNew for Keys<'a, Key, Value>
source§open spec fn ghost_iter(&self) -> KeysGhostIterator<'a, Key, Value>
open spec fn ghost_iter(&self) -> KeysGhostIterator<'a, Key, Value>
{
KeysGhostIterator {
pos: self@.0,
keys: self@.1,
phantom: None,
}
}type GhostIter = KeysGhostIterator<'a, Key, Value>
source§impl<'a, T> ForLoopGhostIteratorNew for Iter<'a, T>
impl<'a, T> ForLoopGhostIteratorNew for Iter<'a, T>
source§open spec fn ghost_iter(&self) -> IterGhostIterator<'a, T>
open spec fn ghost_iter(&self) -> IterGhostIterator<'a, T>
{
IterGhostIterator {
pos: self@.0,
elements: self@.1,
phantom: None,
}
}type GhostIter = IterGhostIterator<'a, T>
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,
}
}