Function extern_spec_T_E_Option_Result_T_E_transpose 

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

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

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

terminates

ghost

ensures

match self {
    None => result == Ok(None),
    Some(Ok(ok)) => result == Ok(Some(ok)),
    Some(Err(err)) => result == Err(err),
}