Struct ScriptedTheorem 

pub struct ScriptedTheorem {
    pub name: String,
    pub premises: Vec<ProofExpr>,
    pub goal: ProofExpr,
    pub script: String,
    pub cites: Vec<String>,
    pub simp: bool,
}

One theorem of a scripted library: proved from its own premises plus the conclusions of the theorems it cites, by running script to a kernel-checked proof. The unit the prove_scripted_library driver discharges in citation order.

Fields

name: String

premises: Vec<ProofExpr>

goal: ProofExpr

script: String

An English-esque proof script (see parse_script).

cites: Vec<String>

Names of earlier theorems whose conclusions this proof relies on.

simp: bool

[simp]-tagged: once proved, this conclusion joins the simp pool and is in scope for every LATER theorem’s simp even without a citation.