Struct TheoremBlock 

pub struct TheoremBlock<'a> {
    pub name: String,
    pub premises: Vec<&'a LogicExpr<'a>>,
    pub premise_names: Vec<Option<String>>,
    pub goal: &'a LogicExpr<'a>,
    pub strategy: ProofStrategy,
}

A theorem block containing premises, goal, and proof strategy.

Fields

name: String

The name of the theorem (e.g., “Socrates_Mortality”)

premises: Vec<&'a LogicExpr<'a>>

Premises (Given statements) - logical expressions to assume true

premise_names: Vec<Option<String>>

Optional names for the premises, parallel to premises. A Given (h): … names that premise h, so a Proof: script can refer to it as cases h rather than the positional hp0. None for an unnamed Given:.

goal: &'a LogicExpr<'a>

The goal to prove (Prove statement)

strategy: ProofStrategy

The proof strategy to use

Trait Implementations

impl<'a> Clone for TheoremBlock<'a>

fn clone(&self) -> TheoremBlock<'a>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'a> Debug for TheoremBlock<'a>

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

Formats the value using the given formatter.