Function vstd::relations::connected

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