Documentation
Lean
.
Linter
.
UnusedVariables
Search
Google site search
Lean
.
Linter
.
UnusedVariables
source
Imports
Init
Lean.Elab.Command
Lean.Linter.Util
Lean.Server.References
Lean.Util.ForEachExprWhere
Imported by
Lean
.
Linter
.
linter
.
unusedVariables
Lean
.
Linter
.
linter
.
unusedVariables
.
funArgs
Lean
.
Linter
.
linter
.
unusedVariables
.
patternVars
Lean
.
Linter
.
getLinterUnusedVariables
Lean
.
Linter
.
getLinterUnusedVariablesFunArgs
Lean
.
Linter
.
getLinterUnusedVariablesPatternVars
Lean
.
Linter
.
IgnoreFunction
Lean
.
Linter
.
builtinUnusedVariablesIgnoreFnsRef
Lean
.
Linter
.
addBuiltinUnusedVariablesIgnoreFn
Lean
.
Linter
.
unusedVariablesIgnoreFnsExt
Lean
.
Linter
.
getUnusedVariablesIgnoreFnsImpl
Lean
.
Linter
.
getUnusedVariablesIgnoreFns
Lean
.
Linter
.
unusedVariables
Lean
.
Linter
.
unusedVariables
.
skipDeclIdIfPresent
Lean
.
Linter
.
unusedVariables
.
isTopLevelDecl
Lean
.
MessageData
.
isUnusedVariableWarning
source
opaque
Lean
.
Linter
.
linter
.
unusedVariables
:
Lean.Option
Bool
source
opaque
Lean
.
Linter
.
linter
.
unusedVariables
.
funArgs
:
Lean.Option
Bool
source
opaque
Lean
.
Linter
.
linter
.
unusedVariables
.
patternVars
:
Lean.Option
Bool
source
def
Lean
.
Linter
.
getLinterUnusedVariables
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
Linter
.
getLinterUnusedVariablesFunArgs
(o :
Lean.Options
)
:
Bool
Instances For
source
def
Lean
.
Linter
.
getLinterUnusedVariablesPatternVars
(o :
Lean.Options
)
:
Bool
Instances For
source
@[inline, reducible]
abbrev
Lean
.
Linter
.
IgnoreFunction
:
Type
Instances For
source
opaque
Lean
.
Linter
.
builtinUnusedVariablesIgnoreFnsRef
:
IO.Ref
(
Array
Lean.Linter.IgnoreFunction
)
source
def
Lean
.
Linter
.
addBuiltinUnusedVariablesIgnoreFn
(ignoreFn :
Lean.Linter.IgnoreFunction
)
:
IO
Unit
Instances For
source
opaque
Lean
.
Linter
.
unusedVariablesIgnoreFnsExt
:
Lean.SimplePersistentEnvExtension
Lake.Name
Unit
source
unsafe def
Lean
.
Linter
.
getUnusedVariablesIgnoreFnsImpl
:
Lean.Elab.Command.CommandElabM
(
Array
Lean.Linter.IgnoreFunction
)
Instances For
source
@[implemented_by Lean.Linter.getUnusedVariablesIgnoreFnsImpl]
opaque
Lean
.
Linter
.
getUnusedVariablesIgnoreFns
:
Lean.Elab.Command.CommandElabM
(
Array
Lean.Linter.IgnoreFunction
)
source
def
Lean
.
Linter
.
unusedVariables
:
Lean.Linter
Instances For
source
def
Lean
.
Linter
.
unusedVariables
.
skipDeclIdIfPresent
(stx :
Lean.Syntax
)
:
Lean.Syntax
Instances For
source
def
Lean
.
Linter
.
unusedVariables
.
isTopLevelDecl
(constDecls :
Lean.HashSet
String.Range
)
:
Lean.Syntax
→
Lean.Syntax.Stack
→
Lean.Options
→
Bool
Instances For
source
def
Lean
.
MessageData
.
isUnusedVariableWarning
(msg :
Lean.MessageData
)
:
Bool
Instances For