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.elabGrindPattern : Command.CommandElab

Equations

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

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

Equations

• Lean.Elab.Tactic.elabResetGrindAttrs x✝ = Lean.Elab.Command.liftTermElabM do liftM Lean.Meta.Grind.resetCasesExt liftM Lean.Meta.Grind.resetEMatchTheoremsExt

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

Equations

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

def Lean.Elab.Tactic.elabGrindParams (params : Meta.Grind.Params) (ps : TSyntaxArray `Lean.Parser.Tactic.grindParam) (only : Bool) : MetaM Meta.Grind.Params

Equations

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

def Lean.Elab.Tactic.elabGrindParams.addEMatchTheorem (params : Meta.Grind.Params) (declName : Name) (kind : Meta.Grind.EMatchTheoremKind) : 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) : 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) (mainDeclName : Name) (fallback : Meta.Grind.Fallback) : MetaM Meta.Grind.Trace

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 ",")) (fallback? : Option Term) : TacticM Meta.Grind.Trace

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.mkGrindOnly (config : TSyntax `Lean.Parser.Tactic.optConfig) (fallback? : Option Term) (trace : Meta.Grind.Trace) : MetaM (TSyntax `tactic)

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.evalGrindTrace : Tactic

Equations

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