Function extern_spec_T_E_Result_T_E_and 

pub fn extern_spec_T_E_Result_T_E_and<T, E, U>(
    self_: Result<T, E>,
    res: Result<U, E>,
) -> Result<U, E>

extern spec for Result<T, E>::and

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

terminates

ghost

ensures

(exists<t: T> self == Ok(t)) ==> result == res

ensures

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