Function extern_spec_T_U_TryInto_U_T_try_into 

pub fn extern_spec_T_U_TryInto_U_T_try_into<T, U: TryFrom<T>>(
    self_: T,
) -> Result<U, U::Error>

extern spec for [T::try_into]

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

requires

U::try_from.precondition((self,))

ensures

U::try_from.postcondition((self,), result)