Enum ProofSystem 

pub enum ProofSystem {
    PRA,
    ECA,
    RobinsonQ,
    PeanoPA,
    Z2,
    Custom(String),
}

Represents a formal proof system in reverse mathematics.

Variants

PRA

Primitive Recursive Arithmetic (PRA).

ECA

Elementary Recursive Arithmetic (ECA).

RobinsonQ

Robinson Arithmetic (Q).

PeanoPA

Peano Arithmetic (PA).

Z2

Second-Order Arithmetic (Z₂).

Custom(String)

A custom-named system.

Implementations

impl ProofSystem

pub fn name(&self) -> String

pub fn is_conservative_over(&self, other: &ProofSystem) -> bool

Returns true if other is provably a conservative extension of self.

pub fn stronger_systems(&self) -> Vec<ProofSystem>

Returns the set of systems stronger than (or equal to) self.

Trait Implementations

impl Clone for ProofSystem

fn clone(&self) -> ProofSystem

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofSystem

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

Formats the value using the given formatter.

impl PartialEq for ProofSystem

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

impl StructuralPartialEq for ProofSystem