Function vstd::set::fold::is_fun_commutative

source · 
pub open spec fn is_fun_commutative<A, B>(f: FnSpec<(B, A), B>) -> bool
Expand description
{ forall |a1, a2, b| #[trigger] f(f(b, a2), a1) == f(f(b, a1), a2) }