vstd::std_specs::cmp

Trait OrdSpec

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

Required Methods§

Source

spec fn obeys_cmp_spec() -> bool

Source

spec 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.

Implementors§

Source§

impl<VERUS_SPEC__A: Ord + ?Sized> OrdSpec for VERUS_SPEC__A