Trait creusot_contracts::std::iter::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<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@ }

Implementors

impl<'a, T> IntoIterator for &'a Option<T>

impl<'a, T> IntoIterator for &'a mut Option<T>

impl<I: Iterator> IntoIterator for I

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>