Skip to main content

ExFromIterator

vstd::std_specs::iter

Trait ExFromIterator 

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

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

Required Associated Types§

Source

type ExternalTraitSpecificationFor: FromIterator<A>

Required Methods§

Source

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

Source

exec fn from_iter<T>(iter: T) -> s : Self
where T: IntoIterator<Item = A>,

ensures
Self::from_iter_ensures(into_iter_remaining(iter), s),

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§