Function extern_spec_T_E_Result_T_E_unwrap_err 

pub fn extern_spec_T_E_Result_T_E_unwrap_err<T, E>(self_: Result<T, E>) -> E
where
    T: Debug,

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

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

terminates

ghost

requires

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

ensures

Err(result) == self