Skip to main content

ExDoubleEndedIterator

vstd::std_specs::iter

Trait ExDoubleEndedIterator 

Source 
pub trait ExDoubleEndedIterator: Iterator {
    type ExternalTraitSpecificationFor: DoubleEndedIterator;

    // Required methods
    exec fn next_back(&mut self) -> ret : Option<<Self as Iterator>::Item>;
    spec fn peek_back(&self, index: int) -> Option<Self::Item>;
}

Required Associated Types§

Source

type ExternalTraitSpecificationFor: DoubleEndedIterator

Required Methods§

Source

exec fn next_back(&mut self) -> ret : Option<<Self as Iterator>::Item>

ensures
<Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self))
    == <Self as IteratorSpec>::obeys_prophetic_iter_laws(old(self)),
<Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self))
    ==> <Self as IteratorSpec>::will_return_none(final(self))
        == <Self as IteratorSpec>::will_return_none(old(self)),
<Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self))
    ==> (<Self as IteratorSpec>::decrease(old(self)) is Some
        <==> <Self as IteratorSpec>::decrease(final(self)) is Some),
<Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self))
    ==> ({
        if <Self as IteratorSpec>::remaining(old(self)).len() > 0 {
            <Self as IteratorSpec>::remaining(final(self))
                == <Self as IteratorSpec>::remaining(old(self)).drop_last()
                && ret == Some(<Self as IteratorSpec>::remaining(old(self)).last())
        } else {
            <Self as IteratorSpec>::remaining(final(self))
                == <Self as IteratorSpec>::remaining(old(self)) && ret == None
                && <Self as IteratorSpec>::will_return_none(final(self))
        }
    }),
<Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self))
    && <Self as IteratorSpec>::remaining(old(self)).len() > 0
    && <Self as IteratorSpec>::decrease(final(self)) is Some
    ==> <Self as IteratorSpec>::decrease(old(self))->0
        > <Self as IteratorSpec>::decrease(final(self))->0,
Source

spec fn peek_back(&self, index: int) -> Option<Self::Item>

Implementors§