Struct ProofExplainer 

pub struct ProofExplainer { /* private fields */ }

Proof explanation generator.

Implementations

impl ProofExplainer

pub fn new() -> Self

Create a new proof explainer with default verbosity.

pub fn with_verbosity(verbosity: Verbosity) -> Self

Create a proof explainer with specific verbosity.

pub fn explain_node(&self, proof: &Proof, node: &ProofNode) -> ExplainedStep

Explain a single proof node.

pub fn explain_proof(&self, proof: &Proof) -> Vec<ExplainedStep>

Explain an entire proof.

pub fn summarize_proof(&self, proof: &Proof) -> String

Generate a step-by-step summary of the proof.

pub fn critical_path(&self, proof: &Proof) -> Vec<ProofNodeId>

Identify the critical path in a proof (longest path from axiom to conclusion).

pub fn analyze_complexity(&self, proof: &Proof) -> ProofComplexity

Analyze proof complexity.

Trait Implementations

impl Default for ProofExplainer

fn default() -> Self

Returns the “default value” for a type.