Function vstd::std_specs::control_flow::ex_option_from_residual
source · pub exec fn ex_option_from_residual<T>(option: Option<Infallible>) -> option2 : Option<T>
Expand description
ensures
option.is_none(),
option2.is_none(),