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

@[reducible, inline]

abbrev Lean.Meta.Grind.TParam : Type

Equations

• Lean.Meta.Grind.TParam = Lean.TSyntax `Lean.Parser.Tactic.grindParam

def Lean.Meta.Grind.mkFinishTactic (seq : List TGrind) (extraParams : Array TParam := #[]) : CoreM TGrind

Given a grind tactic sequence, extracts parameters and builds a terminal finish only tactic. The extraParams are additional parameters (e.g., from the original finish? call) that should always be included.

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) (extraParams : Array TParam := #[]) : 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.

The extraParams are additional parameters (e.g., term arguments from the original grind? call) that should always be included in the suggestion.

Equations

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