def Lean.Elab.Tactic.configElab : Lean.ParserDescr

Equations

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

def Lean.Elab.Tactic.checkConfigElab : Lean.Linter.MissingDocs.SimpleHandler

Equations

• Lean.Elab.Tactic.checkConfigElab = Lean.Linter.MissingDocs.mkSimpleHandler "config elab"