Struct ProofTrace 

pub struct ProofTrace {
    pub goal: String,
    pub steps: Vec<ProofStep>,
}

Trace showing how a goal was proven

Fields

goal: String

Root goal that was proven

steps: Vec<ProofStep>

Steps taken to prove the goal

Implementations

impl ProofTrace

pub fn empty() -> Self

Create an empty proof trace

pub fn new(goal: String) -> Self

Create a new proof trace

pub fn add_step(&mut self, step: ProofStep)

Add a step to the proof

pub fn from_goal(goal: &Goal) -> Self

Build trace from a goal tree

pub fn print(&self)

Print the proof trace in a readable format

Trait Implementations

impl Clone for ProofTrace

fn clone(&self) -> ProofTrace

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofTrace

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

Formats the value using the given formatter.