Function vstd::function::fun_ext

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

General properties of spec functions.

For now, this just contains an axiom of function extensionality for spec_fn. DEPRECATED: use f1 =~= f2 or f1 =~~= f2 instead. Axiom of function extensionality: two functions are equal if they are equal on all inputs.