Trait FromIteratorSpecImpl 

pub trait FromIteratorSpecImpl<A>: Sized + FromIterator<A> {
    // Required method
    exec fn from_iter_ensures(
        remaining: Seq<A>,
        produces: Seq<bool>,
        s: Self,
    ) -> bool;
}

Required Methods

exec fn from_iter_ensures(remaining: Seq<A>, produces: Seq<bool>, s: Self) -> bool

Dyn Compatibility

This trait is not dyn compatible.

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

Implementations on Foreign Types

impl<T> FromIteratorSpecImpl<T> for Vec<T>

open spec fn from_iter_ensures(remaining: Seq<T>, produces: Seq<bool>, s: Self) -> bool

{
    &&& produces.len() == remaining.len()
    &&& produces.all(|p: bool| p)
    &&& remaining == s@

}

Implementors