Function extern_spec_T_E_Result_T_E_unwrap 

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

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

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

terminates

ghost

requires

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

ensures

Ok(result) == self