Trait IntoIterator

pub trait IntoIterator: IntoIterator
where
    Self::IntoIter: Iterator,
{
    // Required method
    fn into_iter_post(self, res: Self::IntoIter) -> bool;

    // Provided method
    fn into_iter_pre(self) -> bool { ... }
}

Required Methods

fn into_iter_post(self, res: Self::IntoIter) -> bool

logic(prophetic)

Provided Methods

fn into_iter_pre(self) -> bool

logic

pearlite! { true }

Implementations on Foreign Types

impl<K: DeepModel, V, S> IntoIterator for &HashMap<K, V, S>

fn into_iter_pre(self) -> bool

logic

pearlite! { true }

fn into_iter_post(self, res: Self::IntoIter) -> bool

logic

pearlite! { self@ == res@ }

impl<K: DeepModel, V, S> IntoIterator for &mut HashMap<K, V, S>

fn into_iter_pre(self) -> bool

logic

pearlite! { true }

fn into_iter_post(self, res: Self::IntoIter) -> bool

logic(prophetic)

pearlite! { forall<k: K::DeepModelTy> (*self)@.contains(k) == (^self)@.contains(k)
&& (forall<k: K::DeepModelTy> (*self)@.contains(k) == res@.contains(k))
&& forall<k: K::DeepModelTy> (*self)@.contains(k) ==> (*self)@[k] == *res@[k] && (^self)@[k] == ^res@[k] }

impl<K: DeepModel, V, S> IntoIterator for HashMap<K, V, S>

fn into_iter_pre(self) -> bool

logic

pearlite! { true }

fn into_iter_post(self, res: Self::IntoIter) -> bool

logic

pearlite! { self@ == res@ }

impl<T> IntoIterator for &[T]

fn into_iter_pre(self) -> bool

logic

pearlite! { true }

fn into_iter_post(self, res: Self::IntoIter) -> bool

logic

pearlite! { self == res@ }

impl<T> IntoIterator for &mut [T]

fn into_iter_pre(self) -> bool

logic

pearlite! { true }

fn into_iter_post(self, res: Self::IntoIter) -> bool

logic

pearlite! { self == res@ }

impl<T, const N: usize> IntoIterator for [T; N]

fn into_iter_pre(self) -> bool

logic

pearlite! { true }

fn into_iter_post(self, res: Self::IntoIter) -> bool

logic(prophetic)

pearlite! { self@ == res@ }

impl<T: DeepModel, S> IntoIterator for &HashSet<T, S>

fn into_iter_pre(self) -> bool

logic

pearlite! { true }

fn into_iter_post(self, res: Self::IntoIter) -> bool

logic

pearlite! { self@ == res@ }

impl<T: DeepModel, S> IntoIterator for HashSet<T, S>

fn into_iter_pre(self) -> bool

logic

pearlite! { true }

fn into_iter_post(self, res: Self::IntoIter) -> bool

logic

pearlite! { self@ == res@ }

Implementors

impl<I: Iterator> IntoIterator for I

impl<T> IntoIterator for &Option<T>

impl<T> IntoIterator for &mut Option<T>

impl<T> IntoIterator for Option<T>

impl<T, A: Allocator> IntoIterator for &VecDeque<T, A>

impl<T, A: Allocator> IntoIterator for &Vec<T, A>

impl<T, A: Allocator> IntoIterator for &mut Vec<T, A>

impl<T, A: Allocator> IntoIterator for Vec<T, A>