Function vstd::relations::irreflexive

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