axiom_fn_mut_call_requires

vstd::function

Function axiom_fn_mut_call_requires 

Source 
pub broadcast proof fn axiom_fn_mut_call_requires<Args: Tuple, F: FnMut<Args>>(
    f: &mut F,
    args: Args,
)
Expand description
requires
call_requires::<Args, F>(mut_ref_current(f), args),
ensures
#[trigger] call_requires::<Args, &mut F>(f, args),