Function vstd::std_specs::control_flow::ex_option_branch

source · 
pub exec fn ex_option_branch<T>(
    option: Option<T>
) -> cf : ControlFlow<<Option<T> as Try>::Residual, <Option<T> as Try>::Output>
Expand description
ensures
cf
    === match option {
        Some(v) => ControlFlow::Continue(v),
        None => ControlFlow::Break(None),
    },