def Lean.Elab.Tactic.elabGrindConfig (cfg : Syntax) (init : Grind.Config := { }) (logExceptions : Bool := true) : TacticM Grind.Config

def Lean.Elab.Tactic.elabGrindConfigInteractive (cfg : Syntax) (init : Grind.ConfigInteractive := { }) (logExceptions : Bool := true) : TacticM Grind.Config

def Lean.Elab.Tactic.elabCutsatConfig (cfg : Syntax) (init : Grind.CutsatConfig := { }) (logExceptions : Bool := true) : TacticM Grind.Config

def Lean.Elab.Tactic.elabLinarithConfig (cfg : Syntax) (init : Grind.LinarithConfig := { }) (logExceptions : Bool := true) : TacticM Grind.Config

def Lean.Elab.Tactic.elabOrderConfig (cfg : Syntax) (init : Grind.OrderConfig := { }) (logExceptions : Bool := true) : TacticM Grind.Config

def Lean.Elab.Tactic.elabGrobnerConfig (cfg : Syntax) (init : Grind.GrobnerConfig := { }) (logExceptions : Bool := true) : TacticM Grind.Config

def Lean.Elab.Tactic.Grind.elabConfigItems (init : Grind.Config) (items : Array Syntax) : TermElabM Grind.Config

def Lean.Elab.Tactic.Grind.withConfigItems {α : Type} (items : Array Syntax) (k : GrindTacticM α) : GrindTacticM α