vstd::std_specs::result

Function spec_unwrap

Source 
pub open spec fn spec_unwrap<T, E: Debug>(result: Result<T, E>) -> T
Expand description
recommends
result is Ok,
{ result->Ok_0 }