FromIteratorSpec

Trait FromIteratorSpec 

Source
pub trait FromIteratorSpec<A>: FromIterator<A> {
    // Required method
    fn from_iter_post(prod: Seq<A>, res: Self) -> bool;
}

Required Methods§

Source

fn from_iter_post(prod: Seq<A>, res: Self) -> bool

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.

Implementations on Foreign Types§

Source§

impl<K: Eq + Hash + DeepModel, V, S: Default + BuildHasher> FromIteratorSpec<(K, V)> for HashMap<K, V, S>

Source§

fn from_iter_post(prod: Seq<(K, V)>, res: Self) -> bool

(open)

pearlite! { forall<k: K::DeepModelTy, v: V> (res@.get(k) == Some(v))
== (exists<i, k1: K> 0 <= i && i < prod.len() && k1.deep_model() == k && prod[i] == (k1, v)
    && forall<j> i < j && j < prod.len() ==> prod[j].0.deep_model() != k) }
Source§

impl<T> FromIteratorSpec<T> for Vec<T>

Source§

fn from_iter_post(prod: Seq<T>, res: Self) -> bool

(open)

pearlite! { prod == res@ }

Source§

impl<T: Eq + Hash + DeepModel, S: Default + BuildHasher> FromIteratorSpec<T> for HashSet<T, S>

Source§

fn from_iter_post(prod: Seq<T>, res: Self) -> bool

(open)

pearlite! { forall<x: T::DeepModelTy> res@.contains(x) == exists<x1: T> x1.deep_model() == x && prod.contains(x1) }

Implementors§