Function extern_spec_T_E_Result_T_E_is_err 

pub fn extern_spec_T_E_Result_T_E_is_err<T, E>(self_: &Result<T, E>) -> bool

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

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

terminates

ghost

ensures

result == exists<e: E> *self == Err(e)