Module rule_search 

aesop-style rule-set search: turn auto’s fixed cascade into an extensible, best-first search over registered rules.

Lean’s aesop lets you register lemmas as intro/elim/forward/destruct rules with priorities and a safe/unsafe classification, then searches best-first. This is that shape, built on the existing tactic combinators and the cheap ProofState clone that already powers backtracking: SAFE rules are applied whenever they fire (no branching — they never lose information); UNSAFE rules fork the search, ordered by priority. A node budget bounds the search, and SearchStats exposes how much was explored — so a best-first strategy can be shown to expand fewer nodes than blind depth-first first/repeat.

auto becomes one rule among many (an unsafe fallback), completing the inversion the tactic framework was built for.

Structs

Rule

A search rule: a named tactic with a role and a safety classification.

RuleSet

An extensible collection of search rules.

SearchStats

What the search explored.

Enums

RuleKind

The role a rule plays (currently advisory metadata for ordering/diagnostics; the tactic itself encodes the actual transformation).

Safety

How a rule participates in search.

Functions

default_ruleset

The default rule set: auto as the sole unsafe fallback — so a default search closes exactly what auto closes, the regression baseline.