Module lemma_index 

exact? / apply? and premise selection: search over a NAMED, certified lemma library.

Each lemma is peeled to ∀xs. A₁ → … → Aₖ → C; its conclusion C is indexed in a discrimination tree (crate::discrimination). A query matches the goal against candidate conclusions with the one-sided matcher (crate::unify::match_expr_pattern) — so a quantified lemma instantiates at the (possibly ground) goal for free. find_exact reports lemmas whose conclusion IS the goal; find_apply reports lemmas whose conclusion matches and lists the antecedents you would still owe. select_premises ranks the whole library for relevance, the premise filter that keeps auto tractable on a large axiom base.

This is the direct answer to Lean’s exact?/apply? and to premise selection — search over a citable, kernel-checkable library rather than an opaque model.

Structs

LemmaIndex

An index over a named lemma library.

Suggestion

A search result: which lemma, the suggested tactic text, the instantiation, and (for apply?) the antecedents still to prove.