Trait OrdLogic 

pub trait OrdLogic: PartialOrdLogic {
    // Required method
    fn lt_log_total(self, other: Self);

    // Provided method
    fn cmp_log(self, other: Self) -> Ordering { ... }
}

Types that implement this trait must have a total order (Ord trait in Rust).

Required Methods

fn lt_log_total(self, other: Self)

The order is total

logic(law)

ensures

self < other || self == other || other < self

Provided Methods

fn cmp_log(self, other: Self) -> Ordering

The comparison operation.

logic(open, sealed)

/* Macro-generated */

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl OrdLogic for bool

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for char

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for i8

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for i16

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for i32

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for i64

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for i128

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for isize

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for u8

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for u16

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for u32

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for u64

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for u128

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl OrdLogic for usize

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl<A: OrdLogic, B: OrdLogic> OrdLogic for (A, B)

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl<T: OrdLogic> OrdLogic for &T

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

impl<T: OrdLogic> OrdLogic for Option<T>

fn lt_log_total(self, other: Self)

logic(law)

ensures

self < other || self == other || other < self

Implementors

impl OrdLogic for Int

impl OrdLogic for Nat

impl OrdLogic for PeanoInt

impl OrdLogic for Positive

impl OrdLogic for PositiveReal

impl OrdLogic for Real

impl<T: OrdLogic> OrdLogic for Seq<T>