Trait DoubleEndedIteratorSpecImpl 

pub trait DoubleEndedIteratorSpecImpl: Iterator + DoubleEndedIterator {
    // Required method
    exec fn peek_back(&self, index: int) -> Option<Self::Item>;
}

Required Methods

exec 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".

Implementations on Foreign Types

impl<'a, T: 'a> DoubleEndedIteratorSpecImpl for Iter<'a, T>

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

{
    if 0 <= index < into_iter_elts(*self).len() {
        Some(&into_iter_elts(*self)[into_iter_elts(*self).len() - index - 1])
    } else {
        None
    }
}

impl<B, I, F> DoubleEndedIteratorSpecImpl for Map<I, F>

where I: DoubleEndedIterator + IteratorSpec, F: FnMut(I::Item) -> B,

open spec fn peek_back(&self, index: int) -> Option<B>

{
    match map_iter(*self).peek_back(index) {
        Some(v) => {
            let x = choose |x| map_fun(*self).ensures((v,), x);
            Some(x)
        }
        None => None,
    }
}

impl<I> DoubleEndedIteratorSpecImpl for Rev<I>

where I: DoubleEndedIterator + IteratorSpec,

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

{ rev_iter(*self).peek(index) }

impl<I> DoubleEndedIteratorSpecImpl for Skip<I>

where I: DoubleEndedIteratorSpec + ExactSizeIteratorSpec,

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

{
    let len = skip_iter(*self).exact_len();
    if len < skip_init_n(*self) || index >= len - skip_init_n(*self) {
        None
    } else {
        skip_iter(*self).peek_back(index)
    }
}

impl<I> DoubleEndedIteratorSpecImpl for Take<I>

where I: DoubleEndedIteratorSpec + ExactSizeIteratorSpec,

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

{
    let len = take_iter(*self).exact_len();
    if len < take_count(*self) {
        None
    } else {
        take_iter(*self).peek_back(len - take_count(*self) - index - 1)
    }
}

impl<T, A: Allocator> DoubleEndedIteratorSpecImpl for IntoIter<T, A>

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

{
    let len = into_iter_elts(*self).len();
    if 0 <= index < len { Some(into_iter_elts(*self)[len - index - 1]) } else { None }
}

Implementors