Struct creusot_contracts::num_rational::Real

pub struct Real(/* private fields */);

Implementations

impl Real

pub fn from_int(_: Int) -> Self

logic

Trait Implementations

impl OrdLogic for Real

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)