opaque Lean.Linter.linter.unusedVariables : Lean.Option Bool

opaque Lean.Linter.linter.unusedVariables.funArgs : Lean.Option Bool

opaque Lean.Linter.linter.unusedVariables.patternVars : Lean.Option Bool

def Lean.Linter.getLinterUnusedVariables (o : Lean.Options) : Bool

Equations

• Lean.Linter.getLinterUnusedVariables o = Lean.Linter.getLinterValue Lean.Linter.linter.unusedVariables o

def Lean.Linter.getLinterUnusedVariablesFunArgs (o : Lean.Options) : Bool

Equations

• Lean.Linter.getLinterUnusedVariablesFunArgs o = Lean.KVMap.get o Lean.Linter.linter.unusedVariables.funArgs.name (Lean.Linter.getLinterUnusedVariables o)

def Lean.Linter.getLinterUnusedVariablesPatternVars (o : Lean.Options) : Bool

Equations

• Lean.Linter.getLinterUnusedVariablesPatternVars o = Lean.KVMap.get o Lean.Linter.linter.unusedVariables.patternVars.name (Lean.Linter.getLinterUnusedVariables o)

@[inline, reducible]

abbrev Lean.Linter.IgnoreFunction : Type

Equations

• Lean.Linter.IgnoreFunction = (Lean.Syntax → Lean.Syntax.Stack → Lean.Options → Bool)

unsafe def Lean.Linter.mkIgnoreFnImpl (constName : Lake.Name) : Lean.ImportM Lean.Linter.IgnoreFunction

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by Lean.Linter.mkIgnoreFnImpl]

opaque Lean.Linter.mkIgnoreFn (constName : Lake.Name) : Lean.ImportM Lean.Linter.IgnoreFunction

opaque Lean.Linter.builtinUnusedVariablesIgnoreFnsRef : IO.Ref (Array Lean.Linter.IgnoreFunction)

def Lean.Linter.addBuiltinUnusedVariablesIgnoreFn (h : Lean.Linter.IgnoreFunction) : IO Unit

Equations

• Lean.Linter.addBuiltinUnusedVariablesIgnoreFn h = ST.Ref.modify Lean.Linter.builtinUnusedVariablesIgnoreFnsRef fun (x : Array Lean.Linter.IgnoreFunction) => Array.push x h

opaque Lean.Linter.unusedVariablesIgnoreFnsExt : Lean.PersistentEnvExtension Lake.Name (Lake.Name × Lean.Linter.IgnoreFunction) (List Lake.Name × Array Lean.Linter.IgnoreFunction)

unsafe def Lean.Linter.getUnusedVariablesIgnoreFnsImpl : Lean.Elab.Command.CommandElabM (Array Lean.Linter.IgnoreFunction)

Equations

• Lean.Linter.getUnusedVariablesIgnoreFnsImpl = do let __do_lift ← Lean.getEnv pure (Lean.PersistentEnvExtension.getState Lean.Linter.unusedVariablesIgnoreFnsExt __do_lift).snd

@[implemented_by Lean.Linter.getUnusedVariablesIgnoreFnsImpl]

opaque Lean.Linter.getUnusedVariablesIgnoreFns : Lean.Elab.Command.CommandElabM (Array Lean.Linter.IgnoreFunction)

def Lean.Linter.unusedVariables : Lean.Linter

Equations

• One or more equations did not get rendered due to their size.

def Lean.Linter.unusedVariables.skipDeclIdIfPresent (stx : Lean.Syntax) : Lean.Syntax

Equations

• Lean.Linter.unusedVariables.skipDeclIdIfPresent stx = if Lean.Syntax.isOfKind stx `Lean.Parser.Command.declId = true then stx[0] else stx

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.

def Lean.MessageData.isUnusedVariableWarning (msg : Lean.MessageData) : Bool

Equations

• Lean.MessageData.isUnusedVariableWarning msg = Lean.MessageData.hasTag (fun (x : Lake.Name) => x == Lean.Linter.linter.unusedVariables.name) msg