Function extern_spec_T_U_Into_U_T_into 

pub fn extern_spec_T_U_Into_U_T_into<T, U>(self_: T) -> U
where
    U: From<T>,

extern spec for [T::into]

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

requires

<U as From<T>>::from.precondition((self,))

ensures

<U as From<T>>::from.postcondition((self,), result)