Function vstd::function::fun_ext_4

source ·
pub fn fun_ext_4<A1, A2, A3, A4, B>(
    f1: FnSpec<(A1, A2, A3, A4), B>,
    f2: FnSpec<(A1, A2, A3, A4), B>
)
👎Deprecated: use f1 =~= f2 or f1 =~~= f2 instead
Expand description
requires
forall |x1: A1, x2: A2, x3: A3, x4: A4| f1(x1, x2, x3, x4) == f2(x1, x2, x3, x4),
ensures
f1 == f2,

DEPRECATED: use f1 =~= f2 or f1 =~~= f2 instead. See fun_ext