Enum ProofStep 

pub enum ProofStep {
    Axiom {
        conclusion: String,
    },
    Inference {
        rule: String,
        premises: SmallVec<[ProofNodeId; 4]>,
        conclusion: String,
        args: SmallVec<[String; 2]>,
    },
}

A single proof step.

Variants

Axiom

Axiom (no premises)

Fields

conclusion: String

The conclusion term

Inference

Inference rule application

Fields

rule: String

Rule name

premises: SmallVec<[ProofNodeId; 4]>

Premise node IDs (optimized for 1-4 premises)

conclusion: String

The conclusion term

args: SmallVec<[String; 2]>

Optional arguments to the rule (optimized for 0-2 args)

Trait Implementations

impl Clone for ProofStep

fn clone(&self) -> ProofStep

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofStep

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

Formats the value using the given formatter.

impl Display for ProofStep

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

Formats the value using the given formatter.