Struct ScopedChecker 

pub struct ScopedChecker { /* private fields */ }

A kernel context prepared ONCE from a scope, against which many candidate derivations can then be checked — the reusable half of check_derivation.

check_derivation rebuilds the standard library, the premise hypotheses and every referenced symbol on every call. That is right for a one-shot trust door and wrong for a SEARCH: crate::tactic::ProofState::by_rule proposes one node per candidate premise tuple and must ask the kernel about each of them. The scope does not change between those questions, so it is built once and the per-question cost is the certification itself.

This is the same check check_derivation performs — certify, infer, compare to the goal — so a tactic that consults it before reporting success cannot hand qed a tree the kernel will refuse.

Implementations

impl ScopedChecker

pub fn new(premises: &[ProofExpr], goal: &ProofExpr) -> Self

Prepare the context for a goal and the facts in scope.

pub fn certifies(&self, derivation: DerivationTree) -> bool

Does this derivation certify as a proof of the scope’s goal?