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