Function vstd::std_specs::option::unwrap

source · 
pub exec fn unwrap<T>(option: Option<T>) -> t : T
Expand description
requires
option.is_Some(),
ensures
t == spec_unwrap(option),