Commands to validate tactic results.

source
def Lean.Elab.CheckTactic.elabCheckTactic :
Command.CommandElab
Equations

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

Instances For

source
def Lean.Elab.CheckTactic.elabCheckTacticFailure :
Command.CommandElab
Equations

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

Instances For

source
def Lean.Elab.CheckTactic.expandCheckSimp :
Macro
Equations

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

Instances For

source
def Lean.Elab.CheckTactic.expandCheckSimpFailure :
Macro
Equations

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

Instances For