Function vstd::relations::commutative

source · 
pub open spec fn commutative<T, U>(r: FnSpec<(T, T), U>) -> bool
Expand description
{ forall |x: T, y: T| #[trigger] r(x, y) == #[trigger] r(y, x) }