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

def Lean.Elab.Tactic.elabGrindConfigInteractive : Syntax → TacticM Grind.ConfigInteractive

def Lean.Elab.Tactic.elabCutsatConfig : Syntax → TacticM Grind.CutsatConfig

def Lean.Elab.Tactic.elabLinarithConfig : Syntax → TacticM Grind.LinarithConfig

def Lean.Elab.Tactic.elabOrderConfig : Syntax → TacticM Grind.OrderConfig

def Lean.Elab.Tactic.elabGrobnerConfig : Syntax → TacticM Grind.GrobnerConfig

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.elabGrindSuggestions (params : Meta.Grind.Params) (suggestions : Array LibrarySuggestions.Suggestion := #[]) : MetaM Meta.Grind.Params

def Lean.Elab.Tactic.elabGrindLocals (params : Meta.Grind.Params) : MetaM Meta.Grind.Params

Add all definitions from the current file.

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

def Lean.Elab.Tactic.grind (mvarId : MVarId) (config : Grind.Config) (only : Bool) (ps : TSyntaxArray `Lean.Parser.Tactic.grindParam) (seq? : Option (TSyntax `Lean.Parser.Tactic.Grind.grindSeq)) : TacticM Unit

def Lean.Elab.Tactic.evalGrindCore (ref : Syntax) (config : Grind.Config) (only : Option Syntax) (params? : Option (Syntax.TSepArray `Lean.Parser.Tactic.grindParam ",")) (seq? : Option (TSyntax `Lean.Parser.Tactic.Grind.grindSeq)) : TacticM Unit

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.filterSuggestionsAndLocalsFromGrindConfig (config : TSyntax `Lean.Parser.Tactic.optConfig) : TSyntax `Lean.Parser.Tactic.optConfig

Filter out +suggestions and +locals from the config syntax

def Lean.Elab.Tactic.evalGrind : Tactic

def Lean.Elab.Tactic.evalGrindTraceCore (stx : Syntax) (trace verbose useSorry : Bool := true) : TacticM (Array (TSyntax `tactic))

def Lean.Elab.Tactic.evalGrindTrace : Tactic

def Lean.Elab.Tactic.evalLia : Tactic

def Lean.Elab.Tactic.evalCutsat : Tactic

def Lean.Elab.Tactic.evalOrder : Tactic

def Lean.Elab.Tactic.evalLinarith : Tactic

def Lean.Elab.Tactic.evalGrobner : Tactic