Enum CertifiablePrimitive 

pub enum CertifiablePrimitive {
    Ring,
    Lia,
    Cc,
}

A tactic reduction primitive a second kernel can now corroborate.

Variants

Ring

try_ring goal ⟶ DRingSolve goal.

Lia

try_lia goal ⟶ DLiaSolve goal.

Cc

try_cc goal ⟶ DccSolve goal.

Implementations

impl CertifiablePrimitive

pub const ALL: [CertifiablePrimitive; 3]

All three, so a census can iterate them without a hand-written list going stale.

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

The reduction-rule name this primitive fires on.

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

The derivation constructor the rule reduces to on success.

pub fn verify(self, goal: &Syn) -> bool

Whether goal is one this primitive genuinely solves, decided independently.

true licenses the caller to reduce <rule> goal to <ctor> goal. false licenses NOTHING — in particular it never licenses reducing to the error derivation, because this module is incomplete on purpose and its silence is not a verdict.

pub fn of_rule(name: &str) -> Option<CertifiablePrimitive>

The primitive a reduction-rule name denotes, if it is one of the three.

Trait Implementations

impl Clone for CertifiablePrimitive

fn clone(&self) -> CertifiablePrimitive

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CertifiablePrimitive

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

Formats the value using the given formatter.

impl PartialEq for CertifiablePrimitive

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

impl Eq for CertifiablePrimitive

impl StructuralPartialEq for CertifiablePrimitive