pub struct MapIterGhostIterator<'a, Key, Value> {
pub pos: int,
pub kv_pairs: Seq<(Key, Value)>,
pub _marker: PhantomData<&'a Key>,
}
Fields§
§pos: int
§kv_pairs: Seq<(Key, Value)>
§_marker: PhantomData<&'a Key>
Trait Implementations§
Source§impl<'a, Key: 'a, Value: 'a> ForLoopGhostIterator for MapIterGhostIterator<'a, Key, Value>
impl<'a, Key: 'a, Value: 'a> ForLoopGhostIterator for MapIterGhostIterator<'a, Key, Value>
Source§open spec fn exec_invariant(&self, exec_iter: &Iter<'a, Key, Value>) -> bool
open spec fn exec_invariant(&self, exec_iter: &Iter<'a, Key, Value>) -> bool
{
&&& self.pos == exec_iter@.0
&&& self.kv_pairs == exec_iter@.1
}
Source§open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool
open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool
{
init matches Some(
init,
) ==> {
&&& init.pos == 0
&&& init.kv_pairs == self.kv_pairs
&&& 0 <= self.pos <= self.kv_pairs.len()
}
}
Source§open spec fn ghost_ensures(&self) -> bool
open spec fn ghost_ensures(&self) -> bool
{ self.pos == self.kv_pairs.len() }
Source§open spec fn ghost_decrease(&self) -> Option<int>
open spec fn ghost_decrease(&self) -> Option<int>
{ Some(self.kv_pairs.len() - self.pos) }
Source§open spec fn ghost_peek_next(&self) -> Option<(Key, Value)>
open spec fn ghost_peek_next(&self) -> Option<(Key, Value)>
{
if 0 <= self.pos < self.kv_pairs.len() {
Some(self.kv_pairs[self.pos])
} else {
None
}
}
Source§open spec fn ghost_advance(
&self,
_exec_iter: &Iter<'a, Key, Value>,
) -> MapIterGhostIterator<'a, Key, Value>
open spec fn ghost_advance( &self, _exec_iter: &Iter<'a, Key, Value>, ) -> MapIterGhostIterator<'a, Key, Value>
{ Self { pos: self.pos + 1, ..*self } }
type ExecIter = Iter<'a, Key, Value>
type Item = (Key, Value)
type Decrease = int
Source§impl<'a, Key, Value> View for MapIterGhostIterator<'a, Key, Value>
impl<'a, Key, Value> View for MapIterGhostIterator<'a, Key, Value>
Source§open spec fn view(&self) -> Seq<(Key, Value)>
open spec fn view(&self) -> Seq<(Key, Value)>
{ self.kv_pairs.take(self.pos) }
type V = Seq<(Key, Value)>
Auto Trait Implementations§
impl<'a, Key, Value> Freeze for MapIterGhostIterator<'a, Key, Value>
impl<'a, Key, Value> RefUnwindSafe for MapIterGhostIterator<'a, Key, Value>where
Key: RefUnwindSafe,
Value: RefUnwindSafe,
impl<'a, Key, Value> Send for MapIterGhostIterator<'a, Key, Value>
impl<'a, Key, Value> Sync for MapIterGhostIterator<'a, Key, Value>
impl<'a, Key, Value> Unpin for MapIterGhostIterator<'a, Key, Value>
impl<'a, Key, Value> UnwindSafe for MapIterGhostIterator<'a, Key, Value>
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more