Enum PropertyDomain 

pub enum PropertyDomain {
    Integers,
    Naturals,
    Booleans,
}

The finite domain a For all property quantified over, with the concrete bound the runner actually enumerated/sampled — the disclosure that keeps a green property from silently meaning “unbounded proof” (G13-full). Carried on the TestOutcome so the inventory can classify a property honestly.

Variants

Integers

For all integers …: — sampled over [-1000, 1000] (infinite domain, so never a proof, even under --prove).

Naturals

For all naturals …: — sampled over [0, 1000] (infinite domain).

Booleans

For all booleans …: — the only FINITE domain, exhausted under --prove.

Implementations

impl PropertyDomain

pub fn bound(self) -> &'static str

The human-readable, disclosed bound ([-1000, 1000] etc.) — what the runner ACTUALLY covered, never a claim of unbounded truth.

pub fn is_finite(self) -> bool

Whether this domain is FINITE — the only domain a property can be PROVED over by exhaustion (booleans). Infinite domains are only ever sampled.

Trait Implementations

impl Clone for PropertyDomain

fn clone(&self) -> PropertyDomain

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for PropertyDomain

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for PropertyDomain

fn eq(&self, other: &PropertyDomain) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for PropertyDomain

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Copy for PropertyDomain

impl Eq for PropertyDomain

impl StructuralPartialEq for PropertyDomain