Function vstd::function::fun_ext_1

source · 
pub fn fun_ext_1<A1, B>(f1: FnSpec<(A1,), B>, f2: FnSpec<(A1,), B>)
👎Deprecated: use f1 =~= f2 or f1 =~~= f2 instead
Expand description
requires
forall |x1: A1| f1(x1) == f2(x1),
ensures
f1 == f2,

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