Documentation

Lean.Linter.Basic

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) :

Equations

Lean.Linter.getLinterUnusedVariables o = Lean.KVMap.get o Lean.Linter.linter.unusedVariables.name (Lean.Linter.getLinterAll o)

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

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) :

Equations

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

def Lean.Linter.unusedVariables:

Equations

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

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

Equations

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

def Lean.Linter.unusedVariables.isTopLevelDecl (constDecls : Std.HashSet String.Range) (stx : Lean.Syntax) (stack : Lean.Linter.SyntaxStack) :

Equations

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

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

Lean.Linter.SyntaxStack → Bool

Equations

Lean.Linter.unusedVariables.matchesUnusedPattern stx x = String.startsWith (Lean.Name.toString (Lean.Syntax.getId stx)) "_"

def Lean.Linter.unusedVariables.isVariable:

Lean.Syntax → Lean.Linter.SyntaxStack → Bool

Equations

Lean.Linter.unusedVariables.isVariable x stack = Lean.Linter.stackMatches stack [some `null, none, some `null, some `Lean.Parser.Command.variable]

def Lean.Linter.unusedVariables.isInStructure:

Lean.Syntax → Lean.Linter.SyntaxStack → Bool

Equations

Lean.Linter.unusedVariables.isInStructure x stack = Lean.Linter.stackMatches stack [some `null, none, some `null, some `Lean.Parser.Command.structure]

def Lean.Linter.unusedVariables.isInInductive:

Lean.Syntax → Lean.Linter.SyntaxStack → Bool

Equations

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

def Lean.Linter.unusedVariables.isInCtorOrStructBinder:

Lean.Syntax → Lean.Linter.SyntaxStack → Bool

Equations

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

def Lean.Linter.unusedVariables.isInConstantOrAxiom:

Lean.Syntax → Lean.Linter.SyntaxStack → Bool

Equations

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

def Lean.Linter.unusedVariables.isInDefWithForeignDefinition:

Lean.Syntax → Lean.Linter.SyntaxStack → Bool

Equations

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

def Lean.Linter.unusedVariables.isInDepArrow:

Lean.Syntax → Lean.Linter.SyntaxStack → Bool

Equations

Lean.Linter.unusedVariables.isInDepArrow x stack = Lean.Linter.stackMatches stack [some `null, some `Lean.Parser.Term.explicitBinder, some `Lean.Parser.Term.depArrow]

def Lean.Linter.unusedVariables.isInLetDeclaration:

Lean.Syntax → Lean.Linter.SyntaxStack → Bool

Equations

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

def Lean.Linter.unusedVariables.isInDeclarationSignature:

Lean.Syntax → Lean.Linter.SyntaxStack → Bool

Equations

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

def Lean.Linter.unusedVariables.isInFun:

Lean.Syntax → Lean.Linter.SyntaxStack → Bool

Equations

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

def Lean.Linter.unusedVariables.isPatternVar:

Lean.Syntax → Lean.Linter.SyntaxStack → Bool

Equations

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