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

Equations

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

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

Equations

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

def Lean.Elab.Tactic.grind (mvarId : Lean.MVarId) (config : Lean.Grind.Config) (mainDeclName : Lean.Name) (fallback : Lean.Meta.Grind.Fallback) : Lean.MetaM Unit

Equations

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

def Lean.Elab.Tactic.evalApplyRfl : Lean.Elab.Tactic.Tactic

Equations

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