pub struct ValuesGhostIterator<'a, Key, Value> {
pub pos: int,
pub values: Seq<Value>,
pub phantom: Option<&'a Key>,
}Fields§
§pos: int§values: Seq<Value>§phantom: Option<&'a Key>Trait Implementations§
Source§impl<'a, Key: 'a, Value: 'a> ForLoopGhostIterator for ValuesGhostIterator<'a, Key, Value>
impl<'a, Key: 'a, Value: 'a> ForLoopGhostIterator for ValuesGhostIterator<'a, Key, Value>
Source§open spec fn exec_invariant(&self, exec_iter: &Values<'a, Key, Value>) -> bool
open spec fn exec_invariant(&self, exec_iter: &Values<'a, Key, Value>) -> bool
{
&&& self.pos == exec_iter@.0
&&& self.values == 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.values == self.values
&&& 0 <= self.pos <= self.values.len()
}
}Source§open spec fn ghost_ensures(&self) -> bool
open spec fn ghost_ensures(&self) -> bool
{ self.pos == self.values.len() }Source§open spec fn ghost_decrease(&self) -> Option<int>
open spec fn ghost_decrease(&self) -> Option<int>
{ Some(self.values.len() - self.pos) }Source§open spec fn ghost_peek_next(&self) -> Option<Value>
open spec fn ghost_peek_next(&self) -> Option<Value>
{ if 0 <= self.pos < self.values.len() { Some(self.values[self.pos]) } else { None } }Source§open spec fn ghost_advance(
&self,
_exec_iter: &Values<'a, Key, Value>,
) -> ValuesGhostIterator<'a, Key, Value>
open spec fn ghost_advance( &self, _exec_iter: &Values<'a, Key, Value>, ) -> ValuesGhostIterator<'a, Key, Value>
{ Self { pos: self.pos + 1, ..*self } }type ExecIter = Values<'a, Key, Value>
type Item = Value
type Decrease = int
Auto Trait Implementations§
impl<'a, Key, Value> Freeze for ValuesGhostIterator<'a, Key, Value>
impl<'a, Key, Value> RefUnwindSafe for ValuesGhostIterator<'a, Key, Value>where
Value: RefUnwindSafe,
Key: RefUnwindSafe,
impl<'a, Key, Value> Send for ValuesGhostIterator<'a, Key, Value>
impl<'a, Key, Value> Sync for ValuesGhostIterator<'a, Key, Value>
impl<'a, Key, Value> Unpin for ValuesGhostIterator<'a, Key, Value>where
Value: Unpin,
impl<'a, Key, Value> UnwindSafe for ValuesGhostIterator<'a, Key, Value>where
Value: UnwindSafe,
Key: RefUnwindSafe,
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