Function vstd::std_specs::result::map

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