Function vstd::std_specs::option::unwrap

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