Struct TheoremCompileResult 

pub struct TheoremCompileResult {
    pub name: String,
    pub premises: Vec<ProofExpr>,
    pub goal: Option<ProofExpr>,
    pub goal_string: Option<String>,
    pub derivation: Option<DerivationTree>,
    pub verified: bool,
    pub verification_error: Option<String>,
    pub answer: Option<Vec<String>>,
    pub grid: Option<SolvedGrid>,
    pub error: Option<String>,
}

Result of compiling and verifying a theorem block.

Contains the parsed theorem structure (name, premises, goal) along with the proof derivation tree if automatic proof search succeeded.

Fields

name: String

The theorem’s declared name.

premises: Vec<ProofExpr>

Compiled premise expressions (axioms).

goal: Option<ProofExpr>

The goal expression to prove, or None on parse error.

goal_string: Option<String>

Simplified FOL string of the goal for display.

derivation: Option<DerivationTree>

Derivation tree from backward chaining, if proof found.

verified: bool

True iff the derivation was certified AND kernel type-checked. A derivation alone (derivation.is_some()) never implies this.

verification_error: Option<String>

Where verification broke (certification or type-check), if it did.

answer: Option<Vec<String>>

For a wh-question goal (“Who is in Florida?”), the certified witness(es); None when the goal is a closed proposition.

grid: Option<SolvedGrid>

For a recognized finite-domain grid, the cells the certified prover could fill — attached whenever the premises take the grid form, no flag required.

error: Option<String>

Error message if compilation or proof failed.

Trait Implementations

impl Clone for TheoremCompileResult

fn clone(&self) -> TheoremCompileResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TheoremCompileResult

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

Formats the value using the given formatter.