Trait ExOrd 

pub trait ExOrd:
    Eq
    + PartialOrd
    + PointeeSized {
    type ExternalTraitSpecificationFor: Ord;

    // Required methods
    spec fn obeys_cmp_spec() -> bool;
    spec fn cmp_spec(&self, other: &Self) -> Ordering;
    exec fn cmp(&self, other: &Self) -> r : Ordering;
    exec fn max(self, other: Self) -> r : Self;
    exec fn min(self, other: Self) -> r : Self;
    exec fn clamp(self, min: Self, max: Self) -> r : Self;
}

Required Associated Types

type ExternalTraitSpecificationFor: Ord

Required Methods

spec fn obeys_cmp_spec() -> bool

spec fn cmp_spec(&self, other: &Self) -> Ordering

exec fn cmp(&self, other: &Self) -> r : Ordering

ensures

Self::obeys_cmp_spec() ==> r == self.cmp_spec(other),

exec fn max(self, other: Self) -> r : Self

ensures

({
    &&& Self::obeys_cmp_spec()
    &&& Self::obeys_partial_cmp_spec()
    &&& other.partial_cmp_spec(&self) == Some(other.cmp_spec(&self))

})
    ==> match other.cmp_spec(&self) {
        Ordering::Less => r == self,
        Ordering::Equal => r == other,
        Ordering::Greater => r == other,
    },

exec fn min(self, other: Self) -> r : Self

ensures

({
    &&& Self::obeys_cmp_spec()
    &&& Self::obeys_partial_cmp_spec()
    &&& other.partial_cmp_spec(&self) == Some(other.cmp_spec(&self))

})
    ==> match other.cmp_spec(&self) {
        Ordering::Less => r == other,
        Ordering::Equal => r == self,
        Ordering::Greater => r == self,
    },

exec fn clamp(self, min: Self, max: Self) -> r : Self

requires

Self::obeys_partial_cmp_spec(),

min.partial_cmp_spec(&max) matches Some(Ordering::Less | Ordering::Equal),

ensures

({
    &&& Self::obeys_cmp_spec()
    &&& Self::obeys_partial_cmp_spec()
    &&& self.partial_cmp_spec(&min) == Some(self.cmp_spec(&min))
    &&& self.partial_cmp_spec(&max) == Some(self.cmp_spec(&max))

})
    ==> match (self.cmp_spec(&min), self.cmp_spec(&max)) {
        (Ordering::Less, _) => r == min,
        (_, Ordering::Greater) => r == max,
        _ => r == self,
    },

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors