vstd::std_specs::cmp

Trait OrdSpecImpl

Source 
pub trait OrdSpecImpl:
    Eq
    + PartialOrd
    + Ord {
    // Required methods
    exec fn obeys_cmp_spec() -> bool;
    exec fn cmp_spec(&self, other: &Self) -> Ordering;
}

Required Methods§

Source

exec fn obeys_cmp_spec() -> bool

Source

exec fn cmp_spec(&self, other: &Self) -> 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 OrdSpecImpl for i8

Source§

open spec fn obeys_cmp_spec() -> bool

{ true }
Source§

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

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

impl OrdSpecImpl for i16

Source§

open spec fn obeys_cmp_spec() -> bool

{ true }
Source§

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

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

impl OrdSpecImpl for i32

Source§

open spec fn obeys_cmp_spec() -> bool

{ true }
Source§

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

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

impl OrdSpecImpl for i64

Source§

open spec fn obeys_cmp_spec() -> bool

{ true }
Source§

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

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

impl OrdSpecImpl for i128

Source§

open spec fn obeys_cmp_spec() -> bool

{ true }
Source§

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

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

impl OrdSpecImpl for isize

Source§

open spec fn obeys_cmp_spec() -> bool

{ true }
Source§

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

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

impl OrdSpecImpl for u8

Source§

open spec fn obeys_cmp_spec() -> bool

{ true }
Source§

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

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

impl OrdSpecImpl for u16

Source§

open spec fn obeys_cmp_spec() -> bool

{ true }
Source§

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

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

impl OrdSpecImpl for u32

Source§

open spec fn obeys_cmp_spec() -> bool

{ true }
Source§

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

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

impl OrdSpecImpl for u64

Source§

open spec fn obeys_cmp_spec() -> bool

{ true }
Source§

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

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

impl OrdSpecImpl for u128

Source§

open spec fn obeys_cmp_spec() -> bool

{ true }
Source§

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

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

impl OrdSpecImpl for usize

Source§

open spec fn obeys_cmp_spec() -> bool

{ true }
Source§

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

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

impl<T: OrdSpec> OrdSpecImpl for Option<T>

Source§

open spec fn obeys_cmp_spec() -> bool

{ T::obeys_cmp_spec() }
Source§

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

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

Implementors§