Struct RealNumber 

pub struct RealNumber {
    pub cauchy_seq: Vec<f64>,
    pub modulus: String,
}

A constructive real number as a Cauchy sequence with a modulus.

Fields

cauchy_seq: Vec<f64>

Approximations: cauchy_seq[n] approximates the real to within 2^{-n}.

modulus: String

A description of the modulus of convergence.

Implementations

impl RealNumber

pub fn new(cauchy_seq: Vec<f64>, modulus: impl Into<String>) -> Self

Create a new RealNumber.

pub fn equality_is_undecidable(&self) -> bool

Equality of constructive reals is co-enumerable (not decidable in general).

pub fn is_apartness_relation(&self) -> bool

Two constructive reals x, y are apart (x # y) if |x - y| > 2^{-n} for some n — this is a positive, decidable relation.