def Lean.Elab.Tactic.elabGrindConfig : Syntax → TacticM Grind.Config

def Lean.Elab.Tactic.elabGrindPattern : Command.CommandElab

def Lean.Elab.Tactic.elabResetGrindAttrs : Command.CommandElab

def Lean.Elab.Tactic.elabInitGrindNorm : Command.CommandElab

def Lean.Elab.Tactic.elabGrindParams (params : Meta.Grind.Params) (ps : TSyntaxArray `Lean.Parser.Tactic.grindParam) (only : Bool) : MetaM Meta.Grind.Params

def Lean.Elab.Tactic.elabGrindParams.addEMatchTheorem (params : Meta.Grind.Params) (declName : Name) (kind : Meta.Grind.EMatchTheoremKind) : MetaM Meta.Grind.Params

def Lean.Elab.Tactic.mkGrindParams (config : Grind.Config) (only : Bool) (ps : TSyntaxArray `Lean.Parser.Tactic.grindParam) : MetaM Meta.Grind.Params

def Lean.Elab.Tactic.grind (mvarId : MVarId) (config : Grind.Config) (only : Bool) (ps : TSyntaxArray `Lean.Parser.Tactic.grindParam) (fallback : Meta.Grind.Fallback) : TacticM Meta.Grind.Trace

def Lean.Elab.Tactic.evalGrindCore (ref : Syntax) (config : Grind.Config) (only : Option Syntax) (params : Option (Syntax.TSepArray `Lean.Parser.Tactic.grindParam ",")) (fallback? : Option Term) : TacticM Meta.Grind.Trace

def Lean.Elab.Tactic.grindParamsPos : Nat

Position for the [..] child syntax in the grind tactic.

def Lean.Elab.Tactic.grindOnlyPos : Nat

Position for the only child syntax in the grind tactic.

def Lean.Elab.Tactic.isGrindOnly (stx : TSyntax `tactic) : Bool

def Lean.Elab.Tactic.setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `tactic

def Lean.Elab.Tactic.getGrindParams (stx : TSyntax `tactic) : Array Syntax

def Lean.Elab.Tactic.mkGrindOnly (config : TSyntax `Lean.Parser.Tactic.optConfig) (fallback? : Option Term) (trace : Meta.Grind.Trace) : MetaM (TSyntax `tactic)

def Lean.Elab.Tactic.evalGrind : Tactic

def Lean.Elab.Tactic.evalGrindTrace : Tactic