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.elabGrindLocals (params : Meta.Grind.Params) : MetaM Meta.Grind.Params

Add all definitions from the current file.

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) (extensions? : Option Meta.Grind.ExtensionStateArray := none) : TermElabM Meta.Grind.Params

Equations

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

def Lean.Elab.Tactic.checkTerminalAsSorry (mvarId : MVarId) : TacticM Bool

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)) (extensions? : Option Meta.Grind.ExtensionStateArray := none) (head? : Option Syntax := none) : 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)) (extensions? : Option Meta.Grind.ExtensionStateArray := none) (head? : Option Syntax := none) : 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.filterSuggestionsAndLocalsFromGrindConfig (config : TSyntax `Lean.Parser.Tactic.optConfig) : TSyntax `Lean.Parser.Tactic.optConfig

Filter out +suggestions and +locals 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.evalSym : 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.evalLia : 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.evalOrder : Tactic

Equations

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

def Lean.Elab.Tactic.evalLinarith : 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.