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.

ghost

requires

self

ensures

self