Documentation

Lean.Meta.Tactic.Grind.Finish

source
@[reducible, inline]
abbrev Lean.Meta.Grind.Action.maxIterationsDefault :
Nat
Equations
Instances For
    source
    def Lean.Meta.Grind.Action.mkFinish (maxIterations : Nat := maxIterationsDefault) :
    IO Action
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For