Trait vstd::pervasive::ForLoopGhostIteratorNewCopy item path

pub trait ForLoopGhostIteratorNew {
    type GhostIter;

    // Required method
    spec fn ghost_iter(&self) -> Self::GhostIter;
}

Required Associated Types§

Required Methods§

Implementations on Foreign Types§

{
    RangeGhostIterator {
        start: self.start,
        cur: self.start,
        end: self.end,
    }
}

Implementors§