source
def Lean.Elab.Tactic.Conv.applySimpResult (result : Meta.Simp.Result) :
TacticM Unit
Equations

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

Instances For

source
def Lean.Elab.Tactic.Conv.evalSimp :
Tactic
Equations

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

Instances For

source
def Lean.Elab.Tactic.Conv.evalSimpTrace :
Tactic
Equations

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

Instances For

source
def Lean.Elab.Tactic.Conv.evalSimpMatch :
Tactic
Equations

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

Instances For

source
def Lean.Elab.Tactic.Conv.evalDSimp :
Tactic
Equations

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

Instances For

source
def Lean.Elab.Tactic.Conv.evalDSimpTrace :
Tactic
Equations

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

Instances For