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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Tactic.elabGrindSuggestions (params : Meta.Grind.Params) (suggestions : Array LibrarySuggestions.Suggestion := #[]) : MetaM Meta.Grind.Params

Equations

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

def Lean.Elab.Tactic.elabGrindParamsAndSuggestions (params : Meta.Grind.Params) (ps : TSyntaxArray `Lean.Parser.Tactic.grindParam) (suggestions : Array LibrarySuggestions.Suggestion := #[]) (only : Bool) (lax : Bool := false) : MetaM Meta.Grind.Params

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

• Lean.Elab.Tactic.grindParamsPos = 3

def Lean.Elab.Tactic.grindOnlyPos : Nat

Position for the only child syntax in the grind tactic.

Equations

• Lean.Elab.Tactic.grindOnlyPos = 2

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

Equations

• Lean.Elab.Tactic.isGrindOnly stx = (stx.raw.getKind == `Lean.Parser.Tactic.grind && !stx.raw[Lean.Elab.Tactic.grindOnlyPos].isNone)

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

Equations

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

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

Equations

• Lean.Elab.Tactic.getGrindParams stx = stx.raw[Lean.Elab.Tactic.grindParamsPos][1].getSepArgs

def Lean.Elab.Tactic.filterSuggestionsFromGrindConfig (config : TSyntax `Lean.Parser.Tactic.optConfig) : TSyntax `Lean.Parser.Tactic.optConfig

Filter out +suggestions from the config syntax

Equations

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

def Lean.Elab.Tactic.evalGrind : Tactic

Equations

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

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

Equations

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

def Lean.Elab.Tactic.evalGrindTrace : Tactic

Equations

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

def Lean.Elab.Tactic.evalCutsat : Tactic

Equations

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

def Lean.Elab.Tactic.evalGrobner : Tactic

Equations

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