Function vstd::std_specs::result::map_err

source · 
pub exec fn map_err<T, E, F, O: FnOnce(E) -> F>(
    result: Result<T, E>,
    op: O
) -> mapped_result : Result<T, F>
Expand description
requires
result.is_err() ==> op.requires((result.get_Err_0(),)),
ensures
result.is_err()
    ==> mapped_result.is_err()
        && op.ensures((result.get_Err_0(),), mapped_result.get_Err_0()),
result.is_ok() ==> mapped_result == Result::<T, F>::Ok(result.get_Ok_0()),