Function vstd::std_specs::control_flow::ex_result_branch
source · pub exec fn ex_result_branch<T, E>(
result: Result<T, E>
) -> cf : ControlFlow<<Result<T, E> as Try>::Residual, <Result<T, E> as Try>::Output>
Expand description
ensures
cf
=== match result {
Ok(v) => ControlFlow::Continue(v),
Err(e) => ControlFlow::Break(Err(e)),
},