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.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.