Function vstd::seq_lib::commutative_foldr

source · 
pub open spec fn commutative_foldr<A, B>(f: FnSpec<(A, B), B>) -> bool
Expand description
{ forall |x: A, y: A, v: B| #[trigger] f(x, f(y, v)) == f(y, f(x, v)) }