Documentation

Lean.Linter.UnusedVariables

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
Equations
source
def Lean.Linter.getLinterUnusedVariablesFunArgs (o : Lean.Options) :
Bool
Equations
source
def Lean.Linter.getLinterUnusedVariablesPatternVars (o : Lean.Options) :
Bool
Equations
source
@[inline]
abbrev Lean.Linter.IgnoreFunction :
Type
Equations
source
opaque Lean.Linter.builtinUnusedVariablesIgnoreFnsRef :
IO.Ref (Array Lean.Linter.IgnoreFunction)
source
def Lean.Linter.addBuiltinUnusedVariablesIgnoreFn (ignoreFn : Lean.Linter.IgnoreFunction) :
IO Unit
Equations
  • One or more equations did not get rendered due to their size.
source
opaque Lean.Linter.unusedVariablesIgnoreFnsExt :
Lean.SimplePersistentEnvExtension Lean.Name Unit
source
unsafe def Lean.Linter.getUnusedVariablesIgnoreFnsImpl :
Lean.Elab.Command.CommandElabM (Array Lean.Linter.IgnoreFunction)
Equations
  • One or more equations did not get rendered due to their size.
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
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Linter.unusedVariables.skipDeclIdIfPresent (stx : Lean.Syntax) :
Lean.Syntax
Equations
source
def Lean.Linter.unusedVariables.isTopLevelDecl (constDecls : Lean.HashSet String.Range) :
Lean.Syntax → Lean.Syntax.Stack → Lean.Options → Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MessageData.isUnusedVariableWarning (msg : Lean.MessageData) :
Bool
Equations