A very simple parameter minimizer.

inductive Lean.Util.ParamMinimizer.Status : Type

Status of the parameter minimizer procedure.

• missing : Status

  Has not found a solution.

• approx : Status

  Found a non minimal solution.

• precise : Status

  Found a precise solution.

def Lean.Util.ParamMinimizer.instInhabitedStatus.default : Status

Equations

• Lean.Util.ParamMinimizer.instInhabitedStatus.default = Lean.Util.ParamMinimizer.Status.missing

instance Lean.Util.ParamMinimizer.instInhabitedStatus : Inhabited Status

Equations

• Lean.Util.ParamMinimizer.instInhabitedStatus = { default := Lean.Util.ParamMinimizer.instInhabitedStatus.default }

instance Lean.Util.ParamMinimizer.instReprStatus : Repr Status

Equations

• Lean.Util.ParamMinimizer.instReprStatus = { reprPrec := Lean.Util.ParamMinimizer.instReprStatus.repr }

def Lean.Util.ParamMinimizer.instReprStatus.repr : Status → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Util.ParamMinimizer.Result : Type

Result type for the parameter minimizer.

• status : Status

  Search outcome (missing, approx, or precise)

• paramMask : Array Bool

  The final parameter bitmask.

• numCalls : Nat

  Number of test invocations performed.

We use throw () to interrupt the search.

def Lean.Util.ParamMinimizer.search {m : Type → Type} [Monad m] (initialMask : Array Bool) (test : Array Bool → m Bool) (maxCalls : Nat := 0) : m Result

Runs the parameter minimization procedure.

Given an initial bitmask initialMask representing the active parameters, and a monotonic predicate test : Array Bool → m Bool, this function searches for the smallest (1-minimal) superset of initialMask that satisfies test.

Execution proceeds in two phases:

1. init – gradually activates parameters until test first succeeds;
2. prune – removes superfluous active parameters while preserving success.

If the search completes without exceeding maxCalls, the result is marked as .precise. If the budget is exceeded but a valid configuration was found, the result is .approx. If no configuration satisfies test, the result is .missing.

maxCalls = 0 disables the call budget limit.

Equations

• One or more equations did not get rendered due to their size.