Trait OrdLogic 

pub trait OrdLogic {
    // Required methods
    fn cmp_log(self, other: Self) -> Ordering;
    fn cmp_le_log(x: Self, y: Self);
    fn cmp_lt_log(x: Self, y: Self);
    fn cmp_ge_log(x: Self, y: Self);
    fn cmp_gt_log(x: Self, y: Self);
    fn refl(x: Self);
    fn trans(x: Self, y: Self, z: Self, o: Ordering);
    fn antisym1(x: Self, y: Self);
    fn antisym2(x: Self, y: Self);
    fn eq_cmp(x: Self, y: Self);

    // Provided methods
    fn le_log(self, o: Self) -> bool { ... }
    fn lt_log(self, o: Self) -> bool { ... }
    fn ge_log(self, o: Self) -> bool { ... }
    fn gt_log(self, o: Self) -> bool { ... }
}

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

Types that implement this trait must have a total order. In particular, the order must be:

• reflexive
• transitive
• antisymmetric (part1, part2)

Required Methods

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

The comparison operation. Returns:

• Ordering::Less if self is smaller than other
• Ordering::Equal if self is equal to other
• Ordering::Greater if self is greater than other

logic

fn cmp_le_log(x: Self, y: Self)

logic(law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

Reflexivity of the order

logic(law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

Transitivity of the order

logic(law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

Antisymmetry of the order (x < y ==> !(y < x))

The antisymmetry is in two part; here is the second part.

logic(law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

Antisymmetry of the order (x > y ==> !(y > x))

The antisymmetry is in two part; here is the first part.

logic(law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

Compatibility between Ordering::Equal and equality (==).

logic(law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

Provided Methods

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

The logical <= operation.

logic(open)

self.cmp_log(o) != Ordering::Greater

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

The logical < operation.

logic(open)

self.cmp_log(o) == Ordering::Less

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

The logical >= operation.

logic(open)

self.cmp_log(o) != Ordering::Less

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

The logical > operation.

logic(open)

self.cmp_log(o) == Ordering::Greater

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

impl OrdLogic for bool

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for char

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for i8

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for i16

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for i32

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for i64

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for i128

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for isize

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for u8

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for u16

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for u32

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for u64

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for u128

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl OrdLogic for usize

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

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

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

logic(open)

let r = self.0.cmp_log(o.0);
if r == Ordering::Equal {
    self.1.cmp_log(o.1)
} else {
    r
}

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

logic(open)

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

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

logic(open)

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

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

logic(open)

(self.0 == o.0 && self.1 >= o.1) || self.0 > o.0

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

logic(open)

(self.0 == o.0 && self.1 > o.1) || self.0 > o.0

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

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

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

logic(open)

match (self, o) {
    (None, None) => Ordering::Equal,
    (None, Some(_)) => Ordering::Less,
    (Some(_), None) => Ordering::Greater,
    (Some(x), Some(y)) => x.cmp_log(y),
}

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl<T: OrdLogic> OrdLogic for &T

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

logic(open)

T::cmp_log(*self, *o)

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

impl<T: OrdLogic> OrdLogic for Reverse<T>

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

logic(open)

match self.0.cmp_log(o.0) {
    Ordering::Equal => Ordering::Equal,
    Ordering::Less => Ordering::Greater,
    Ordering::Greater => Ordering::Less,
}

fn cmp_le_log(x: Self, y: Self)

logic(open, law)

/* Macro-generated */

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open, law)

/* Macro-generated */

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open, law)

/* Macro-generated */

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open, law)

/* Macro-generated */

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(open, law)

/* Macro-generated */

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open, law)

/* Macro-generated */

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open, law)

/* Macro-generated */

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open, law)

/* Macro-generated */

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open, law)

/* Macro-generated */

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

Implementors

impl OrdLogic for PeanoInt

impl OrdLogic for PositiveReal

impl OrdLogic for Real

impl OrdLogic for Int