Function extern_spec_FromIterator__tuple0__tuple0_from_iter 

pub fn extern_spec_FromIterator__tuple0__tuple0_from_iter<T: IntoIterator<Item = (), IntoIter: IteratorSpec>>(
    iter: T,
)

extern spec for [()::from_iter]

This is not a real function: its only use is for documentation.

requires

T::into_iter.precondition((iter,))

ensures

exists<into_iter: T::IntoIter, prod: Seq<()>, done: &mut T::IntoIter>
    T::into_iter.postcondition((iter,), into_iter) &&
    into_iter.produces(prod, *done) && done.completed() && resolve(^done)