Trait ExactSizeIteratorSpec 

pub trait ExactSizeIteratorSpec: ExactSizeIterator + IteratorSpec {
    // Required method
    fn size_hint_exact(&self, r: (usize, Option<usize>));
}

Required Methods

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

Dyn Compatibility

This trait is not dyn compatible.

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

Implementations on Foreign Types

impl ExactSizeIteratorSpec for Range<i8>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl ExactSizeIteratorSpec for Range<i16>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl ExactSizeIteratorSpec for Range<i32>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl ExactSizeIteratorSpec for Range<isize>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl ExactSizeIteratorSpec for Range<u8>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl ExactSizeIteratorSpec for Range<u16>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl ExactSizeIteratorSpec for Range<u32>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl ExactSizeIteratorSpec for Range<usize>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl ExactSizeIteratorSpec for RangeInclusive<i8>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl ExactSizeIteratorSpec for RangeInclusive<i16>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl ExactSizeIteratorSpec for RangeInclusive<u8>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl ExactSizeIteratorSpec for RangeInclusive<u16>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<'a, I: ExactSizeIteratorSpec<Item = &'a T>, T: Clone + 'a> ExactSizeIteratorSpec for Cloned<I>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<'a, I: ExactSizeIteratorSpec<Item = &'a T>, T: Copy + 'a> ExactSizeIteratorSpec for Copied<I>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<'a, I: ExactSizeIteratorSpec> ExactSizeIteratorSpec for Enumerate<I>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<'a, K: DeepModel, V> ExactSizeIteratorSpec for Iter<'a, K, V>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<'a, K: DeepModel, V> ExactSizeIteratorSpec for IterMut<'a, K, V>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<'a, T: DeepModel> ExactSizeIteratorSpec for Iter<'a, T>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<'a, T> ExactSizeIteratorSpec for Iter<'a, T>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<'a, T> ExactSizeIteratorSpec for Iter<'a, T>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<'a, T> ExactSizeIteratorSpec for IterMut<'a, T>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<A: ExactSizeIteratorSpec, B: ExactSizeIteratorSpec> ExactSizeIteratorSpec for Zip<A, B>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<I: ExactSizeIteratorSpec + ?Sized> ExactSizeIteratorSpec for &mut I

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<I: ExactSizeIteratorSpec + DoubleEndedIteratorSpec> ExactSizeIteratorSpec for Rev<I>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<I: ExactSizeIteratorSpec, B, F: FnMut(I::Item) -> B> ExactSizeIteratorSpec for Map<I, F>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<I: ExactSizeIteratorSpec> ExactSizeIteratorSpec for Fuse<I>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<I: ExactSizeIteratorSpec> ExactSizeIteratorSpec for Skip<I>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<I: ExactSizeIteratorSpec> ExactSizeIteratorSpec for Take<I>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<K: DeepModel, V, A: Allocator> ExactSizeIteratorSpec for IntoIter<K, V, A>

Available on crate feature nightly only.

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

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

Available on crate feature nightly only.

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<T, const N: usize> ExactSizeIteratorSpec for IntoIter<T, N>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<T: DeepModel, A: Allocator> ExactSizeIteratorSpec for IntoIter<T, A>

Available on crate feature nightly only.

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<T> ExactSizeIteratorSpec for Empty<T>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<T> ExactSizeIteratorSpec for IntoIter<T>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<T> ExactSizeIteratorSpec for Iter<'_, T>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<T> ExactSizeIteratorSpec for IterMut<'_, T>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

impl<T> ExactSizeIteratorSpec for Once<T>

fn size_hint_exact(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

r.1 == Some(r.0)

Implementors

impl<I: ExactSizeIteratorSpec + IteratorSpec, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B> ExactSizeIteratorSpec for MapInv<I, F>