Skip to main content

DoubleEndedIteratorSpecImpl

vstd::std_specs::iter

Trait DoubleEndedIteratorSpecImpl 

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

Required Methods§

Source

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

Implementations on Foreign Types§

Source§

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

Source§

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
    }
}
Source§

impl<I> DoubleEndedIteratorSpecImpl for Rev<I>
where I: DoubleEndedIterator + IteratorSpec,

Source§

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

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

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

Source§

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§