Trait vstd::pervasive::ForLoopGhostIteratorCopy item path

pub trait ForLoopGhostIterator {
    type ExecIter;
    type Item;
    type Decrease;

    // Required methods
    spec fn exec_invariant(&self, exec_iter: &Self::ExecIter) -> bool;
    spec fn ghost_invariant(&self, init: Option<&Self>) -> bool;
    spec fn ghost_ensures(&self) -> bool;
    spec fn ghost_decrease(&self) -> Option<Self::Decrease>;
    spec fn ghost_peek_next(&self) -> Option<Self::Item>;
    spec fn ghost_advance(&self, exec_iter: &Self::ExecIter) -> Self
       where Self: Sized;
}

Required Associated Types§

Required Methods§

Object Safety§

Implementors§