vstd::std_specs::cmp

Trait ExPartialOrd

Source 
pub trait ExPartialOrd<Rhs: ?Sized = Self>: PartialEq<Rhs> {
    type ExternalTraitSpecificationFor: PartialOrd<Rhs>;

    // Required methods
    spec fn obeys_partial_cmp_spec() -> bool;
    spec fn partial_cmp_spec(&self, other: &Rhs) -> Option<Ordering>;
    exec fn partial_cmp(&self, other: &Rhs) -> r : Option<Ordering>;
    exec fn lt(&self, other: &Rhs) -> r : bool;
    exec fn le(&self, other: &Rhs) -> r : bool;
    exec fn gt(&self, other: &Rhs) -> r : bool;
    exec fn ge(&self, other: &Rhs) -> r : bool;
}

Required Associated Types§

Source

type ExternalTraitSpecificationFor: PartialOrd<Rhs>

Required Methods§

Source

spec fn obeys_partial_cmp_spec() -> bool

Source

spec fn partial_cmp_spec(&self, other: &Rhs) -> Option<Ordering>

Source

exec fn partial_cmp(&self, other: &Rhs) -> r : Option<Ordering>

ensures
Self::obeys_partial_cmp_spec() ==> r == self.partial_cmp_spec(other),
Source

exec fn lt(&self, other: &Rhs) -> r : bool

ensures
Self::obeys_partial_cmp_spec()
    ==> (r <==> self.partial_cmp_spec(other) == Some(Ordering::Less)),
Source

exec fn le(&self, other: &Rhs) -> r : bool

ensures
Self::obeys_partial_cmp_spec()
    ==> (r
        <==> self.partial_cmp_spec(other) matches Some(Ordering::Less | Ordering::Equal)),
Source

exec fn gt(&self, other: &Rhs) -> r : bool

ensures
Self::obeys_partial_cmp_spec()
    ==> (r <==> self.partial_cmp_spec(other) == Some(Ordering::Greater)),
Source

exec fn ge(&self, other: &Rhs) -> r : bool

ensures
Self::obeys_partial_cmp_spec()
    ==> (r
        <==> self
            .partial_cmp_spec(other) matches Some(Ordering::Greater | Ordering::Equal)),

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§