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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.Tactic.Grind.elabConfigItems init items = Lean.Elab.Tactic.elabGrindConfigCore✝ (fun (c : Lean.Term) => Lean.Elab.ConfigEval.evalExprWithElab c) (Lean.mkNullNode items) init false

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

Equations

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