Trait PartialOrdLogic 

pub trait PartialOrdLogic {
    // Required methods
    fn lt_log(self, other: Self) -> bool;
    fn irreflexive(self);
    fn transitive(x: Self, y: Self, z: Self);
    fn le_lt_log(self, other: Self);

    // Provided methods
    fn gt_log(self, other: Self) -> bool { ... }
    fn le_log(self, other: Self) -> bool { ... }
    fn ge_log(self, other: Self) -> bool { ... }
    fn partial_cmp_log(self, other: Self) -> Option<Ordering> { ... }
}

Trait for comparison operations (<, >, <=, >=) in Pearlite.

Types that implement this trait must satisfy some properties (see PartialOrd trait in Rust).

In particular, the order must be:

• irreflexive
• transitive

Required Methods

fn lt_log(self, other: Self) -> bool

The logical < operation.

logic

fn irreflexive(self)

logic(law)

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic(law)

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic(law)

ensures

(self <= other) == (self < other || self == other)

Provided Methods

fn gt_log(self, other: Self) -> bool

The logical > operation.

logic(open, sealed, inline)

other < self

fn le_log(self, other: Self) -> bool

The logical <= operation.

logic(open, inline)

self < other || self == other

fn ge_log(self, other: Self) -> bool

The logical >= operation.

logic(open, sealed, inline)

other <= self

fn partial_cmp_log(self, other: Self) -> Option<Ordering>

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 PartialOrdLogic for bool

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for char

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for f32

fn lt_log(self, _: Self) -> bool

Note: the implementation of f32::le_log is not the <= operator in Rust, because it is reflexive.

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for f64

fn lt_log(self, _: Self) -> bool

Note: the implementation of f64::le_log is not the <= operator in Rust, because it is reflexive.

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for i8

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for i16

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for i32

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for i64

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for i128

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for isize

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for u8

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for u16

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for u32

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for u64

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for u128

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

impl PartialOrdLogic for usize

fn le_log(self, _: Self) -> bool

logic

fn lt_log(self, _: Self) -> bool

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

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

fn lt_log(self, o: Self) -> bool

logic(open)

self.0 == o.0 && self.1 < o.1 || self.0 < o.0

fn le_log(self, o: Self) -> bool

logic(open)

self.0 == o.0 && self.1 <= o.1 || self.0 < o.0

fn irreflexive(self)

logic(law)

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic(law)

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic(law)

ensures

(self <= other) == (self < other || self == other)

impl<T: PartialOrdLogic> PartialOrdLogic for &T

fn lt_log(self, other: Self) -> bool

logic(open, inline)

*self < *other

fn le_log(self, other: Self) -> bool

logic(open, inline)

*self <= *other

fn irreflexive(self)

logic(law)

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic(law)

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic(law)

ensures

(self <= other) == (self < other || self == other)

impl<T: PartialOrdLogic> PartialOrdLogic for Option<T>

fn lt_log(self, o: Self) -> bool

logic(open)

/* Macro-generated */

fn le_log(self, o: Self) -> bool

logic(open)

/* Macro-generated */

fn irreflexive(self)

logic(law)

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic(law)

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic(law)

ensures

(self <= other) == (self < other || self == other)

impl<T: PartialOrdLogic> PartialOrdLogic for Reverse<T>

fn lt_log(self, o: Self) -> bool

logic(open, inline)

o.0 < self.0

fn le_log(self, o: Self) -> bool

logic(open, inline)

o.0 <= self.0

fn irreflexive(self)

logic(law)

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic(law)

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic(law)

ensures

(self <= other) == (self < other || self == other)

Implementors

impl PartialOrdLogic for Int

impl PartialOrdLogic for Nat

impl PartialOrdLogic for PeanoInt

impl PartialOrdLogic for Positive

impl PartialOrdLogic for PositiveReal

impl PartialOrdLogic for Real

impl PartialOrdLogic for SyncView

impl<T: PartialOrdLogic> PartialOrdLogic for Seq<T>