Enum PremiseVariables 

pub enum PremiseVariables {
    Schematic,
    Local,
}

What a FREE VARIABLE in a knowledge-base equation means.

The chainer serves two callers with two different answers, and the answer is a property of where the knowledge base CAME FROM, not of the search:

• Equations handed straight to BackwardChainer::add_axiom are a REWRITE SYSTEM. A Peano definition — Add(Zero, n) = n, Add(Succ k, n) = Succ(Add(k, n)) — says nothing at all unless it stands for every instance; read as facts about one fixed k and one fixed n, the pair does not compute 1 + 1. Nothing downstream re-checks such a search, and this is what a standalone chainer is for, so it is the default.
• Premises of a THEOREM are KERNEL HYPOTHESES. The trust door registers each as a declaration h : P n whose type mentions n as a context LOCAL — Lean’s variable (n : Int) — and verify::close_over_context_locals closes the finished term over exactly those. An INSTANCE of such a hypothesis is a proposition the context does not carry, so no certificate can cite it. A layer whose success is re-checked must therefore read premises AS STATED: the step is not merely uncertifiable, it is not licensed.

Saying which reading is in force is what keeps the honesty invariant STRUCTURAL. The alternative — letting the search build the step and catching it downstream — is the one answer that is wrong either way: a tactic reports a proof and the trust door refuses it.

Variants

Schematic

An equation stands for ALL its instances (a rewrite schema). The default.

Local

An equation is about the fixed, arbitrary values its free variables name, so only the equation AS STATED is available. Set by every caller whose result the kernel re-checks.

Trait Implementations

impl Clone for PremiseVariables

fn clone(&self) -> PremiseVariables

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PremiseVariables

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

Formats the value using the given formatter.

impl Default for PremiseVariables

fn default() -> PremiseVariables

Returns the “default value” for a type.

impl PartialEq for PremiseVariables

fn eq(&self, other: &PremiseVariables) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for PremiseVariables

impl Eq for PremiseVariables

impl StructuralPartialEq for PremiseVariables