Instances For
@[implemented_by Lean.Linter.MissingDocs.mkHandlerUnsafe]
def
Lean.Linter.MissingDocs.addHandler
(env : Lean.Environment)
(declName : Lake.Name)
(key : Lake.Name)
(h : Lean.Linter.MissingDocs.Handler)
:
Instances For
Instances For
def
Lean.Linter.MissingDocs.addBuiltinHandler
(key : Lake.Name)
(h : Lean.Linter.MissingDocs.Handler)
:
Instances For
Instances For
Instances For
Instances For
def
Lean.Linter.MissingDocs.lintStructField
(parent : Lean.Syntax)
(stx : Lean.Syntax)
(msg : String)
: