Documentation
Lean
.
Elab
.
Tactic
.
Config
Search
Google site search
return to top
source
Imports
Init
Lean.Elab.SyntheticMVars
Lean.Linter.MissingDocs
Lean.Meta.Eval
Lean.Elab.Tactic.Basic
Imported by
Lean
.
Elab
.
Tactic
.
configElab
Lean
.
Elab
.
Tactic
.
checkConfigElab
source
def
Lean
.
Elab
.
Tactic
.
configElab
:
Lean.ParserDescr
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Lean
.
Elab
.
Tactic
.
checkConfigElab
:
Lean.Linter.MissingDocs.SimpleHandler
Equations
Lean.Elab.Tactic.checkConfigElab
=
Lean.Linter.MissingDocs.mkSimpleHandler
"config elab"
Instances For