Documentation
Lean
.
Elab
.
Tactic
.
Config
Search
Google site search
Lean
.
Elab
.
Tactic
.
Config
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
Instances For
source
def
Lean
.
Elab
.
Tactic
.
checkConfigElab
:
Lean.Linter.MissingDocs.SimpleHandler
Instances For