Documentation
Lean
.
Linter
.
MissingDocs
Search
return to top
source
Imports
Lean.Elab.Command
Lean.Elab.SetOption
Lean.Linter.Util
Lean.Parser.Syntax
Lean.Meta.Tactic.Simp.RegisterCommand
Imported by
Lean
.
Linter
.
linter
.
missingDocs
Lean
.
Linter
.
getLinterMissingDocs
Lean
.
Linter
.
MissingDocs
.
SimpleHandler
Lean
.
Linter
.
MissingDocs
.
Handler
Lean
.
Linter
.
MissingDocs
.
SimpleHandler
.
toHandler
Lean
.
Linter
.
MissingDocs
.
mkHandlerUnsafe
Lean
.
Linter
.
MissingDocs
.
mkHandler
Lean
.
Linter
.
MissingDocs
.
builtinHandlersRef
Lean
.
Linter
.
MissingDocs
.
missingDocsExt
Lean
.
Linter
.
MissingDocs
.
addHandler
Lean
.
Linter
.
MissingDocs
.
getHandlers
Lean
.
Linter
.
MissingDocs
.
missingDocs
Lean
.
Linter
.
MissingDocs
.
addBuiltinHandler
Lean
.
Linter
.
MissingDocs
.
lint
Lean
.
Linter
.
MissingDocs
.
lintNamed
Lean
.
Linter
.
MissingDocs
.
lintField
Lean
.
Linter
.
MissingDocs
.
lintStructField
Lean
.
Linter
.
MissingDocs
.
hasInheritDoc
Lean
.
Linter
.
MissingDocs
.
declModifiersPubNoDoc
Lean
.
Linter
.
MissingDocs
.
lintDeclHead
Lean
.
Linter
.
MissingDocs
.
checkDecl
Lean
.
Linter
.
MissingDocs
.
checkInit
Lean
.
Linter
.
MissingDocs
.
checkNotation
Lean
.
Linter
.
MissingDocs
.
checkMixfix
Lean
.
Linter
.
MissingDocs
.
checkSyntax
Lean
.
Linter
.
MissingDocs
.
mkSimpleHandler
Lean
.
Linter
.
MissingDocs
.
checkSyntaxAbbrev
Lean
.
Linter
.
MissingDocs
.
checkSyntaxCat
Lean
.
Linter
.
MissingDocs
.
checkMacro
Lean
.
Linter
.
MissingDocs
.
checkElab
Lean
.
Linter
.
MissingDocs
.
checkClassAbbrev
Lean
.
Linter
.
MissingDocs
.
checkSimpLike
Lean
.
Linter
.
MissingDocs
.
checkRegisterBuiltinOption
Lean
.
Linter
.
MissingDocs
.
checkRegisterOption
Lean
.
Linter
.
MissingDocs
.
checkRegisterSimpAttr
Lean
.
Linter
.
MissingDocs
.
handleIn
Lean
.
Linter
.
MissingDocs
.
handleMutual
source
opaque
Lean
.
Linter
.
linter
.
missingDocs
:
Lean.Option
Bool
source
def
Lean
.
Linter
.
getLinterMissingDocs
(
o
:
LinterOptions
)
:
Bool
Equations
Instances For
source
@[reducible, inline]
abbrev
Lean
.
Linter
.
MissingDocs
.
SimpleHandler
:
Type
Equations
Instances For
source
@[reducible, inline]
abbrev
Lean
.
Linter
.
MissingDocs
.
Handler
:
Type
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
SimpleHandler
.
toHandler
(
h
:
SimpleHandler
)
:
Handler
Equations
Instances For
source
unsafe def
Lean
.
Linter
.
MissingDocs
.
mkHandlerUnsafe
(
constName
:
Name
)
:
ImportM
Handler
Equations
Instances For
source
@[implemented_by Lean.Linter.MissingDocs.mkHandlerUnsafe]
opaque
Lean
.
Linter
.
MissingDocs
.
mkHandler
(
constName
:
Name
)
:
ImportM
Handler
source
opaque
Lean
.
Linter
.
MissingDocs
.
builtinHandlersRef
:
IO.Ref
(
NameMap
Handler
)
source
opaque
Lean
.
Linter
.
MissingDocs
.
missingDocsExt
:
PersistentEnvExtension
(
Name
×
Name
) (
Name
×
Name
×
Handler
) (
List
(
Name
×
Name
)
×
NameMap
Handler
)
source
def
Lean
.
Linter
.
MissingDocs
.
addHandler
(
env
:
Environment
)
(
declName
key
:
Name
)
(
h
:
Handler
)
:
Environment
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
getHandlers
(
env
:
Environment
)
:
NameMap
Handler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
missingDocs
:
Linter
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
addBuiltinHandler
(
key
:
Name
)
(
h
:
Handler
)
:
IO
Unit
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
lint
(
stx
:
Syntax
)
(
msg
:
String
)
:
Elab.Command.CommandElabM
Unit
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
lintNamed
(
stx
:
Syntax
)
(
msg
:
String
)
:
Elab.Command.CommandElabM
Unit
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
lintField
(
parent
stx
:
Syntax
)
(
msg
:
String
)
:
Elab.Command.CommandElabM
Unit
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
lintStructField
(
parent
stx
:
Syntax
)
(
msg
:
String
)
:
Elab.Command.CommandElabM
Unit
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
hasInheritDoc
(
attrs
:
Syntax
)
:
Bool
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
declModifiersPubNoDoc
(
mods
:
Syntax
)
:
Bool
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
lintDeclHead
(
k
:
SyntaxNodeKind
)
(
id
:
Syntax
)
:
Elab.Command.CommandElabM
Unit
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkDecl
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkInit
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkNotation
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkMixfix
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkSyntax
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
mkSimpleHandler
(
name
:
String
)
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkSyntaxAbbrev
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkSyntaxCat
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkMacro
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkElab
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkClassAbbrev
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkSimpLike
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkRegisterBuiltinOption
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkRegisterOption
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
checkRegisterSimpAttr
:
SimpleHandler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
handleIn
:
Handler
Equations
Instances For
source
def
Lean
.
Linter
.
MissingDocs
.
handleMutual
:
Handler
Equations
Instances For