@[reducible, inline]

abbrev Lean.Meta.Grind.Action.maxIterationsDefault : Nat

Equations

• Lean.Meta.Grind.Action.maxIterationsDefault = 10000

def Lean.Meta.Grind.Action.mkFinish (maxIterations : Nat := maxIterationsDefault) : IO Action

The finish action: introduces hypotheses, asserts all pending facts, and then repeats the solvers, E-matching, case-splitting, and model-based theory combination until the goal is closed, no step applies, or maxIterations is reached.

The action does not validate the script it generates when tracing. Callers that report the script (e.g., grind? and finish?) replay it at the goal they consider appropriate.

Equations

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