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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

Reflexivity of the order

law

ensures

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

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

Transitivity of the order

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.

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.

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 (==).

law

ensures

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

Provided Methods

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

The logical <= operation.

logic

pearlite! { self.cmp_log(o) != Ordering::Greater }

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

The logical < operation.

logic

pearlite! { self.cmp_log(o) == Ordering::Less }

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

The logical >= operation.

logic

pearlite! { self.cmp_log(o) != Ordering::Less }

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

The logical > operation.

logic

pearlite! { 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

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for char

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for i8

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for i16

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for i32

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for i64

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for i128

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for isize

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for u8

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for u16

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for u32

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for u64

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for u128

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

impl OrdLogic for usize

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

logic

if self < o {
    Ordering::Less
} else if self == o {
    Ordering::Equal
} else {
    Ordering::Greater
}

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)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: 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

pearlite! { {
    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

pearlite! { (self.0 == o.0 && self.1 <= o.1) || self.0 < o.0 }

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

logic

pearlite! { (self.0 == o.0 && self.1 < o.1) || self.0 < o.0 }

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

logic

pearlite! { (self.0 == o.0 && self.1 >= o.1) || self.0 > o.0 }

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

logic

pearlite! { (self.0 == o.0 && self.1 > o.1) || self.0 > o.0 }

fn cmp_le_log(x: Self, y: Self)

law

ensures

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

fn cmp_lt_log(x: Self, y: Self)

law

ensures

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

fn cmp_ge_log(x: Self, y: Self)

law

ensures

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

fn cmp_gt_log(x: Self, y: Self)

law

ensures

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

fn refl(x: Self)

law

ensures

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

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

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)

law

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

law

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

law

ensures

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

Implementors

impl OrdLogic for Real

impl OrdLogic for Int

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

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