vstd::std_specs::cmp

Trait PartialOrdSpecImpl

Source 
pub trait PartialOrdSpecImpl<Rhs: ?Sized = Self>: PartialEq<Rhs> + PartialOrd<Rhs> {
    // Required methods
    exec fn obeys_partial_cmp_spec() -> bool;
    exec fn partial_cmp_spec(&self, other: &Rhs) -> Option<Ordering>;
}

Required Methods§

Source

exec fn obeys_partial_cmp_spec() -> bool

Source

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

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.

Implementations on Foreign Types§

Source§

impl PartialOrdSpecImpl for i8

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ true }
Source§

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

{
    if *self < *other {
        Some(Ordering::Less)
    } else if *self > *other {
        Some(Ordering::Greater)
    } else {
        Some(Ordering::Equal)
    }
}
Source§

impl PartialOrdSpecImpl for i16

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ true }
Source§

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

{
    if *self < *other {
        Some(Ordering::Less)
    } else if *self > *other {
        Some(Ordering::Greater)
    } else {
        Some(Ordering::Equal)
    }
}
Source§

impl PartialOrdSpecImpl for i32

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ true }
Source§

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

{
    if *self < *other {
        Some(Ordering::Less)
    } else if *self > *other {
        Some(Ordering::Greater)
    } else {
        Some(Ordering::Equal)
    }
}
Source§

impl PartialOrdSpecImpl for i64

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ true }
Source§

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

{
    if *self < *other {
        Some(Ordering::Less)
    } else if *self > *other {
        Some(Ordering::Greater)
    } else {
        Some(Ordering::Equal)
    }
}
Source§

impl PartialOrdSpecImpl for i128

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ true }
Source§

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

{
    if *self < *other {
        Some(Ordering::Less)
    } else if *self > *other {
        Some(Ordering::Greater)
    } else {
        Some(Ordering::Equal)
    }
}
Source§

impl PartialOrdSpecImpl for isize

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ true }
Source§

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

{
    if *self < *other {
        Some(Ordering::Less)
    } else if *self > *other {
        Some(Ordering::Greater)
    } else {
        Some(Ordering::Equal)
    }
}
Source§

impl PartialOrdSpecImpl for u8

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ true }
Source§

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

{
    if *self < *other {
        Some(Ordering::Less)
    } else if *self > *other {
        Some(Ordering::Greater)
    } else {
        Some(Ordering::Equal)
    }
}
Source§

impl PartialOrdSpecImpl for u16

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ true }
Source§

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

{
    if *self < *other {
        Some(Ordering::Less)
    } else if *self > *other {
        Some(Ordering::Greater)
    } else {
        Some(Ordering::Equal)
    }
}
Source§

impl PartialOrdSpecImpl for u32

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ true }
Source§

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

{
    if *self < *other {
        Some(Ordering::Less)
    } else if *self > *other {
        Some(Ordering::Greater)
    } else {
        Some(Ordering::Equal)
    }
}
Source§

impl PartialOrdSpecImpl for u64

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ true }
Source§

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

{
    if *self < *other {
        Some(Ordering::Less)
    } else if *self > *other {
        Some(Ordering::Greater)
    } else {
        Some(Ordering::Equal)
    }
}
Source§

impl PartialOrdSpecImpl for u128

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ true }
Source§

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

{
    if *self < *other {
        Some(Ordering::Less)
    } else if *self > *other {
        Some(Ordering::Greater)
    } else {
        Some(Ordering::Equal)
    }
}
Source§

impl PartialOrdSpecImpl for usize

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ true }
Source§

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

{
    if *self < *other {
        Some(Ordering::Less)
    } else if *self > *other {
        Some(Ordering::Greater)
    } else {
        Some(Ordering::Equal)
    }
}
Source§

impl<T: PartialOrdSpec> PartialOrdSpecImpl for Option<T>

Source§

open spec fn obeys_partial_cmp_spec() -> bool

{ T::obeys_partial_cmp_spec() }
Source§

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

{
    match (self, other) {
        (None, None) => Some(core::cmp::Ordering::Equal),
        (None, Some(_)) => Some(core::cmp::Ordering::Less),
        (Some(_), None) => Some(core::cmp::Ordering::Greater),
        (Some(x), Some(y)) => x.partial_cmp_spec(y),
    }
}

Implementors§