Enum RMStrength 

pub enum RMStrength {
    RCA0,
    BetweenRCA0AndWKL0,
    WKL0,
    BetweenWKL0AndACA0,
    ACA0,
    BetweenACA0AndATR0,
    ATR0,
    Pi11CA0,
    AbovePi11CA0,
    Unknown,
}

Strength classification for a combinatorial principle in the RM zoo.

Variants

RCA0

Provable in RCA₀.

BetweenRCA0AndWKL0

Strictly between RCA₀ and WKL₀.

WKL0

Equivalent to WKL₀ over RCA₀.

BetweenWKL0AndACA0

Strictly between WKL₀ and ACA₀.

ACA0

Equivalent to ACA₀ over RCA₀.

BetweenACA0AndATR0

Strictly between ACA₀ and ATR₀.

ATR0

Equivalent to ATR₀ over RCA₀.

Pi11CA0

Equivalent to Π¹_1-CA₀ over RCA₀.

AbovePi11CA0

Strictly above all Big Five (requires additional set-existence).

Unknown

Strength not yet determined.

Implementations

impl RMStrength

pub fn lower_bound_system(&self) -> Option<BigFiveSystem>

Return the closest Big Five system from below (or None if below RCA₀).

Trait Implementations

impl Clone for RMStrength

fn clone(&self) -> RMStrength

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RMStrength

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

Formats the value using the given formatter.

impl PartialEq for RMStrength

fn eq(&self, other: &RMStrength) -> 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 Eq for RMStrength

impl StructuralPartialEq for RMStrength