Function extern_spec_T_E_Result_Option_T_E_transpose 

pub fn extern_spec_T_E_Result_Option_T_E_transpose<T, E>(
    self_: Result<Option<T>, E>,
) -> Option<Result<T, E>>

extern spec for Result<Option<T>, E>::transpose

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

terminates

ghost

ensures

self == Ok(None) ==> result == None

ensures

forall<t: T> self == Ok(Some(t)) ==> result == Some(Ok(t))

ensures

forall<e: E> self == Err(e) ==> result == Some(Err(e))