vstd::std_specs::cmp

Trait ExOrd

Source 
pub trait ExOrd: Eq + PartialOrd {
    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§

Source

type ExternalTraitSpecificationFor: Ord

Required Methods§

Source

spec fn obeys_cmp_spec() -> bool

Source

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

Source

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

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

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

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

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

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

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()
    ==> 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", so this trait is not object safe.

Implementors§