Trait ExDoubleEndedIterator 

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

type ExternalTraitSpecificationFor: DoubleEndedIterator

Required Methods

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

ensures

iter_state_preserved!(old(self), final(self)),

<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()
            &&& <Self as IteratorSpec>::produces(final(self))
                == <Self as IteratorSpec>::produces(old(self)).drop_last()
            &&& ret == Some(<Self as IteratorSpec>::remaining(old(self)).last())
            &&& <Self as IteratorSpec>::produces(old(self)).last()

        } else {
            &&& <Self as IteratorSpec>::remaining(final(self))
                == <Self as IteratorSpec>::remaining(old(self))
            &&& <Self as IteratorSpec>::produces(final(self))
                == <Self as IteratorSpec>::produces(old(self))
            &&& ret == None

        }
    }),

<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,

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

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors