Function extern_spec_core_iter_Iterator_chain 

pub fn extern_spec_core_iter_Iterator_chain<Self_, U>(
    self_: Self_,
    other: U,
) -> Chain<Self_, U::IntoIter>
where
    Self_: Sized + IteratorSpec + ?Sized + Iterator,
    U: IntoIterator<Item = Self_::Item>,

extern spec for ::core::iter::Iterator::chain<U>

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

ghost

requires

U::into_iter.precondition((other,))

ensures

result.iter_a() == Some(self)

ensures

match result.iter_b() {
    Some(b) => U::into_iter.postcondition((other,), b),
    None => false
}