pub struct IntoIterGhostIterator<T, A: Allocator> {
pub pos: int,
pub elements: Seq<T>,
pub _marker: PhantomData<A>,
}
Fields§
§pos: int
§elements: Seq<T>
§_marker: PhantomData<A>
Trait Implementations§
Source§impl<T, A: Allocator> ForLoopGhostIterator for IntoIterGhostIterator<T, A>
impl<T, A: Allocator> ForLoopGhostIterator for IntoIterGhostIterator<T, A>
Source§open spec fn exec_invariant(&self, exec_iter: &IntoIter<T, A>) -> bool
open spec fn exec_invariant(&self, exec_iter: &IntoIter<T, A>) -> 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: &IntoIter<T, A>,
) -> IntoIterGhostIterator<T, A>
open spec fn ghost_advance( &self, _exec_iter: &IntoIter<T, A>, ) -> IntoIterGhostIterator<T, A>
{ Self { pos: self.pos + 1, ..*self } }
type ExecIter = IntoIter<T, A>
type Item = T
type Decrease = int
Auto Trait Implementations§
impl<T, A> Freeze for IntoIterGhostIterator<T, A>
impl<T, A> RefUnwindSafe for IntoIterGhostIterator<T, A>where
A: RefUnwindSafe,
T: RefUnwindSafe,
impl<T, A> Send for IntoIterGhostIterator<T, A>
impl<T, A> Sync for IntoIterGhostIterator<T, A>
impl<T, A> Unpin for IntoIterGhostIterator<T, A>
impl<T, A> UnwindSafe for IntoIterGhostIterator<T, A>where
A: UnwindSafe,
T: UnwindSafe,
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