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

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.

(open)

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

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

The logical < operation.

(open)

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

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

The logical >= operation.

(open)

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

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

The logical > operation.

(open)

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for char

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for i8

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for i16

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for i32

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for i64

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for i128

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for isize

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for u8

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for u16

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for u32

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for u64

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for u128

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(open(pub(self)), law)

ensures

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

impl OrdLogic for usize

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

(open)

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

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(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

(open)

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

(open)

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

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

(open)

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

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

(open)

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

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

(open)

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(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

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

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(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

(open)

T::cmp_log(*self, *o)

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

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

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

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

fn cmp_le_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open(pub(self)), law)

ensures

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

fn refl(x: Self)

(open(pub(self)), law)

ensures

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

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

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

(open(pub(self)), law)

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

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

(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

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

(open, law)

{}

ensures

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

fn cmp_lt_log(x: Self, y: Self)

(open, law)

{}

ensures

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

fn cmp_ge_log(x: Self, y: Self)

(open, law)

{}

ensures

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

fn cmp_gt_log(x: Self, y: Self)

(open, law)

{}

ensures

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

fn refl(x: Self)

(open, law)

{}

ensures

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

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

(open, 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)

(open, law)

{}

requires

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

ensures

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

fn antisym2(x: Self, y: Self)

(open, law)

{}

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

(open, law)

{}

ensures

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

Implementors

impl OrdLogic for PeanoInt

impl OrdLogic for Real

impl OrdLogic for Int