Struct NativeDecisions 

pub struct NativeDecisions { /* private fields */ }

The native decisions of one export.

Implementations

impl NativeDecisions

pub fn read(export: &str) -> NativeDecisions

Recognize every leaf of export. An export that never names Lean.ofReduceBool costs one substring scan. Nothing is refused here: an export the tables cannot read has no leaves, and the importer reports what is wrong with it.

pub fn is_empty(&self) -> bool

Whether the export has no leaf.

pub fn decisions(&self) -> impl Iterator<Item = &NativeDecision>

Every leaf, in expression order.

pub fn rederive(&self, record: Value) -> Value

The expression record LOGOS reads in place of record: a leaf’s premise applied to Lean’s evaluation step itself, of_decide_eq_true p inst (Eq.refl.{1} Bool Bool.true). Every other record is returned as it is.

pub fn rederivations(&self) -> Vec<Rederivation>

Every declaration whose type or value holds a leaf, in export order.

pub fn closure_of(&self, target: &str) -> Elimination

The closure of target (a kernel name) as Lean’s #print axioms walks it — a definition, theorem or opaque through its type and value, an inductive through its type and constructors, a constructor or recursor through its type, an axiom not at all — with every leaf read as its re-derivation.

pub fn explain(&self, verdict: Verdict, declaration: Option<usize>) -> Verdict

verdict, saying which of the failing declaration’s steps were re-derived: a native decision the kernel refutes or cannot finish is named, never left to look like an unrelated mismatch.