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
Instances For
    source
    def Lean.Linter.getLinterUnusedVariablesFunArgs (o : Lean.Options) :
    Bool
    Equations
    Instances For
      source
      def Lean.Linter.getLinterUnusedVariablesPatternVars (o : Lean.Options) :
      Bool
      Equations
      Instances For
        source
        @[inline, reducible]
        abbrev Lean.Linter.IgnoreFunction :
        Type
        Equations
        Instances For
          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.
          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)
            Equations
            • One or more equations did not get rendered due to their size.
            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
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Lean.Linter.unusedVariables.skipDeclIdIfPresent (stx : Lean.Syntax) :
                Lean.Syntax
                Equations
                Instances For
                  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.
                  Instances For
                    source
                    def Lean.MessageData.isUnusedVariableWarning (msg : Lean.MessageData) :
                    Bool
                    Equations
                    Instances For