Struct LemmaIndex 

pub struct LemmaIndex { /* private fields */ }

An index over a named lemma library.

Implementations

impl LemmaIndex

pub fn build(named: &[(String, ProofExpr)]) -> Self

Build the index from named lemmas (axioms and proved theorems alike).

pub fn find_exact(&self, goal: &ProofExpr) -> Vec<Suggestion>

Lemmas whose conclusion IS the goal (an instance of it). Ranked most- specific first (fewest variable bindings). exact?.

pub fn find_apply(&self, goal: &ProofExpr) -> Vec<Suggestion>

Lemmas whose conclusion matches the goal AND have antecedents — applying them reduces the goal to those (instantiated) antecedents. apply?.

pub fn select_premises(&self, goal: &ProofExpr, k: usize) -> Vec<String>

Rank the whole library by relevance to goal and return the top k names — the premise filter for auto on a large base. Relevance is: an exact/apply conclusion match first, then head-symbol overlap; lemmas sharing no symbol with the goal are dropped entirely.