axiom_fn_mut_call_ensures

vstd::function

Function axiom_fn_mut_call_ensures 

Source 
pub broadcast proof fn axiom_fn_mut_call_ensures<Args: Tuple, F: FnMut<Args>>(
    f: &mut F,
    args: Args,
    output: F::Output,
)
Expand description
requires
#[trigger] call_ensures::<Args, &mut F>(f, args, output),
ensures
call_ensures::<Args, F>(mut_ref_current(f), args, output),
mut_ref_current(f) == mut_ref_future(f),