Function vstd::relations::is_maximal

source · 
pub open spec fn is_maximal<T>(leq: FnSpec<(T, T), bool>, max: T, s: Set<T>) -> bool
Expand description
{
    s.contains(max)
        && forall |x: T| {
            s.contains(x) && #[trigger] leq(max, x) ==> #[trigger] leq(x, max)
        }
}

An element in an ordered set is called a maximal element, if no other element is greater than it.