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> ForLoopGhostIteratorNew for Chars<'a>
impl<'a> ForLoopGhostIteratorNew for Chars<'a>
Source§open spec fn ghost_iter(&self) -> CharsGhostIterator<'a>
open spec fn ghost_iter(&self) -> CharsGhostIterator<'a>
{
CharsGhostIterator {
pos: self@.0,
chars: self@.1,
phantom: None,
}
}type GhostIter = CharsGhostIterator<'a>
Source§impl<'a, Key> ForLoopGhostIteratorNew for Iter<'a, Key>
impl<'a, Key> ForLoopGhostIteratorNew for Iter<'a, Key>
Source§open spec fn ghost_iter(&self) -> SetIterGhostIterator<'a, Key>
open spec fn ghost_iter(&self) -> SetIterGhostIterator<'a, Key>
{
SetIterGhostIterator {
pos: self@.0,
elements: self@.1,
phantom: None,
}
}type GhostIter = SetIterGhostIterator<'a, Key>
Source§impl<'a, Key, Value> ForLoopGhostIteratorNew for Iter<'a, Key, Value>
impl<'a, Key, Value> ForLoopGhostIteratorNew for Iter<'a, Key, Value>
Source§open spec fn ghost_iter(&self) -> MapIterGhostIterator<'a, Key, Value>
open spec fn ghost_iter(&self) -> MapIterGhostIterator<'a, Key, Value>
{
MapIterGhostIterator {
pos: self@.0,
kv_pairs: self@.1,
_marker: PhantomData,
}
}type GhostIter = MapIterGhostIterator<'a, Key, Value>
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, Key, Value> ForLoopGhostIteratorNew for Values<'a, Key, Value>
impl<'a, Key, Value> ForLoopGhostIteratorNew for Values<'a, Key, Value>
Source§open spec fn ghost_iter(&self) -> ValuesGhostIterator<'a, Key, Value>
open spec fn ghost_iter(&self) -> ValuesGhostIterator<'a, Key, Value>
{
ValuesGhostIterator {
pos: self@.0,
values: self@.1,
phantom: None,
}
}type GhostIter = ValuesGhostIterator<'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, 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,
}
}type GhostIter = RangeGhostIterator<A>
Source§impl<T, A: Allocator> ForLoopGhostIteratorNew for IntoIter<T, A>
impl<T, A: Allocator> ForLoopGhostIteratorNew for IntoIter<T, A>
Source§open spec fn ghost_iter(&self) -> IntoIterGhostIterator<T, A>
open spec fn ghost_iter(&self) -> IntoIterGhostIterator<T, A>
{
IntoIterGhostIterator {
pos: self@.0,
elements: self@.1,
_marker: PhantomData,
}
}