Trait ExFromIterator 

pub trait ExFromIterator<A>: Sized {
    type ExternalTraitSpecificationFor: FromIterator<A>;

    // Required methods
    spec fn from_iter_ensures(
        remaining: Seq<A>,
        produces: Seq<bool>,
        s: Self,
    ) -> bool;
    exec fn from_iter<T>(iter: T) -> s : Self
       where T: IntoIterator<Item = A>;
}

Required Associated Types

type ExternalTraitSpecificationFor: FromIterator<A>

Required Methods

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

exec fn from_iter<T>(iter: T) -> s : Self

where T: IntoIterator<Item = A>,

ensures

exists |initial: T::IntoIter| {
    #[trigger] (T::into_iter).ensures((iter,), initial)
        && (initial.obeys_prophetic_iter_laws()
            ==> Self::from_iter_ensures(initial.remaining(), initial.produces(), s))
},

Dyn Compatibility

This trait is not dyn compatible.

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

Implementors