Given an auto-generated grind tactic script, collect params for single shot finish or top-level grind tactic.

def Lean.Meta.Grind.mkFinishTactic (seq : List TGrind) : CoreM TGrind

Given a grind tactic sequence, extracts parameters and builds an terminal finish only tactic.

Equations

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

def Lean.Meta.Grind.mkGrindOnlyTactics (cfg : TSyntax `Lean.Parser.Tactic.optConfig) (seq : List TGrind) : CoreM (Array (TSyntax `tactic))

Given a grind tactic sequence, extracts parameters and builds a grind only tactics. It returns at most two. The first tactic uses anchors to restrict the search if applicable. The second does not restrict the search using anchors. The second option is included only if there are anchors.

Equations

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