Documentation
Lean
.
Elab
.
Tactic
.
Config
Search
Google site search
return to top
source
Imports
Lean.Elab.SyntheticMVars
Lean.Linter.MissingDocs
Lean.Meta.Eval
Lean.Elab.Tactic.Basic
Imported by
Lean.Elab.Tactic.Omega.Frontend
Lean.Elab.Tactic.Rewrite
Lean.Elab.Tactic.Simp
Batteries.Tactic.Congr
Lean.Elab.Tactic.SolveByElim
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.
source
def
Lean
.
Elab
.
Tactic
.
checkConfigElab
:
Lean.Linter.MissingDocs.SimpleHandler
Equations
Lean.Elab.Tactic.checkConfigElab
=
Lean.Linter.MissingDocs.mkSimpleHandler
"config elab"