vstd::std_specs::option

Function spec_expect

Source 
pub open spec fn spec_expect<T>(option: Option<T>, msg: &str) -> T
Expand description
recommends
option is Some,
{ option->0 }