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§

source

spec fn exec_invariant(&self, exec_iter: &Self::ExecIter) -> bool

source

spec fn ghost_invariant(&self, init: Option<&Self>) -> bool

source

spec fn ghost_ensures(&self) -> bool

source

spec fn ghost_decrease(&self) -> Option<Self::Decrease>

source

spec fn ghost_peek_next(&self) -> Option<Self::Item>

source

spec fn ghost_advance(&self, exec_iter: &Self::ExecIter) -> Self
where Self: Sized,

Object Safety§

This trait is not object safe.

Implementors§