vstd::std_specs::option

Function spec_unwrap

Source 
pub open spec fn spec_unwrap<T>(option: Option<T>) -> T
Expand description
recommends
option.is_Some(),
{ option.get_Some_0() }