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