Function extern_spec_std_iter_DoubleEndedIterator_next_back 

pub fn extern_spec_std_iter_DoubleEndedIterator_next_back<Self_>(
    self_: &mut Self_,
) -> Option<Self_::Item>
where
    Self_: DoubleEndedIteratorSpec + ?Sized + DoubleEndedIterator,

extern spec for ::std::iter::DoubleEndedIterator::next_back

This is not a real function: its only use is for documentation.

ensures

match result {
                    None => self.completed(),
                    Some(v) => (*self).produces_back(Seq::singleton(v), ^self)
                }