Documentation
Lean
.
Elab
.
ErrorExplanation
Search
return to top
source
Imports
Lean.ErrorExplanation
Lean.Elab.Command
Lean.Elab.Term
Lean.Meta.Eval
Lean.Widget.UserWidget
Imported by
Lean
.
Elab
.
ErrorExplanation
.
expandNamedErrorMacro
Lean
.
Elab
.
ErrorExplanation
.
elabCheckedNamedError
Lean
.
Elab
.
ErrorExplanation
.
elabRegisterErrorExplanation
source
def
Lean
.
Elab
.
ErrorExplanation
.
expandNamedErrorMacro
:
Macro
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Lean
.
Elab
.
ErrorExplanation
.
elabCheckedNamedError
:
Term.TermElab
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Lean
.
Elab
.
ErrorExplanation
.
elabRegisterErrorExplanation
:
Command.CommandElab
Equations
One or more equations did not get rendered due to their size.
Instances For