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