Struct PositiveReal 

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

Natural numbers, i.e., integers that are greater or equal to 0.

Implementations

impl PositiveReal

pub fn to_real(self) -> Real

ensures

result > Real::from_int(0)

pub fn new(n: Real) -> PositiveReal

requires

n > Real::from_int(0)

ensures

result.to_real() == n

pub fn ext_eq(self, other: Self) -> bool

(open)

let _ = Subset::<PositiveRealInner>::inner_inj;
self.to_real() == other.to_real()

ensures

result == (self == other)

pub fn from_int(i: Int) -> Self

(open, inline)

Self::new(Real::from_int(i))

Trait Implementations

impl AddLogic for PositiveReal

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

ensures

result.to_real() == self.to_real() + other.to_real()

type Output = PositiveReal

impl DivLogic for PositiveReal

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

ensures

result.to_real() == self.to_real() / other.to_real()

type Output = PositiveReal

impl MulLogic for PositiveReal

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

ensures

result.to_real() == self.to_real() * other.to_real()

type Output = PositiveReal

impl RA for PositiveReal

fn op(self, other: Self) -> Option<PositiveReal>

(open, inline)

Some(self + other)

fn factor(self, factor: Self) -> Option<Self>

(open, inline)

let _ = PositiveReal::ext_eq;
if self.to_real() > factor.to_real() {
    Some(PositiveReal::new(self.to_real() - factor.to_real()))
} else {
    None
}

ensures

match result {
        Some(c) => factor.op(c) == Some(self),
        None => forall<c: Self> factor.op(c) != Some(self),
    }

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

(open, inline)

self.ext_eq(other)

ensures

result == (self == other)

fn commutative(a: Self, b: Self)

(law)

ensures

a.op(b) == b.op(a)

fn associative(a: Self, b: Self, c: Self)

ensures

a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc))

fn core(self) -> Option<Self>

(open, inline)

None

fn core_idemp(self)

requires

self.core() != None

ensures

let c = self.core().unwrap_logic();
c.op(c) == Some(c)

ensures

self.core().unwrap_logic().op(self) == Some(self)

fn core_is_maximal_idemp(self, i: Self)

requires

i.op(i) == Some(i)

requires

i.op(self) == Some(self)

ensures

match self.core() {
        Some(c) => i.incl(c),
        None => false,
    }

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

Inclusion of RA.

fn incl_op(self, other: Self, comb: Self)

(law)

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

(open, sealed)

fn incl_eq_op(a: Self, b: Self, x: Self) -> bool

(open, sealed)

fn update(self, x: Self) -> bool

Ensures that we can go from self to x without making composition with the frame invalid.

fn update_nondet(self, s: Set<Self>) -> bool

This is used in Resource::update_nondet.

fn associative_none(a: Self, b: Self, c: Self, bc: Self)

Specialized version of Self::associative, in the case where a.op(b) == None.

fn associative_some(a: Self, b: Self, c: Self, ab: Self, bc: Self)

Specialized version of Self::associative, in the case where a.op(b) and b.op(c) are both valid.

fn incl_transitive(a: Self, b: Self, c: Self)

RA::incl is transitive.