Struct Real 

pub struct Real;

Implementations

impl Real

pub fn from_int(_: Int) -> Self

logic

Trait Implementations

impl AddLogic for Real

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

logic

type Output = Real

impl DivLogic for Real

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

logic

type Output = Real

impl MulLogic for Real

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

logic

type Output = Real

impl NegLogic for Real

fn neg_logic(self) -> Self

logic

type Output = Real

impl OrdLogic for Real

fn lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

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

The comparison operation.

impl PartialOrdLogic for Real

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

logic

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

logic

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

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

The logical > operation.

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

The logical >= operation.

fn partial_cmp_log(self, other: Self) -> Option<Ordering>

logic(open, sealed)

impl SubLogic for Real

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

logic

type Output = Real