Function extern_spec_T_E_Result_T_E_err 

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

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

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

terminates

ghost

ensures

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

ensures

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