Function vstd::std_specs::result::unwrap

source · 
pub exec fn unwrap<T, E: Debug>(result: Result<T, E>) -> t : T
Expand description
requires
result.is_Ok(),
ensures
t == result.get_Ok_0(),