Struct Real 

pub struct Real;

Implementations

impl Real

pub fn from_int(_: Int) -> Self

logic

Trait Implementations

impl AddLogic for Real

fn add(self, other: Self) -> Self

logic

type Output = Real

impl DivLogic for Real

fn div(self, other: Self) -> Self

logic

type Output = Real

impl MulLogic for Real

fn mul(self, other: Self) -> Self

logic

type Output = Real

impl NegLogic for Real

fn neg(self) -> Self

logic

type Output = Real

impl OrdLogic for Real

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 SubLogic for Real

fn sub(self, other: Self) -> Self

logic

type Output = Real