Style linters

This file contains (currently one, eventually more) linters about stylistic aspects: these are only about coding style, but do not affect correctness nor global coherence of mathlib.

Historically, these were ported from the lint-style.py Python script.

opaque Mathlib.Linter.linter.setOption : Lean.Option Bool

The setOption linter emits a warning on a set_option command, term or tactic which sets a pp, profiler or trace option.

def Mathlib.Linter.Style.SetOption.parse_set_option : Lean.Syntax → Option Lean.Name

Whether a syntax element is a set_option command, tactic or term: Return the name of the option being set, if any.

Equations

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

def Mathlib.Linter.Style.SetOption.is_set_option : Lean.Syntax → Bool

Whether a given piece of syntax is a set_option command, tactic or term.

Equations

• Mathlib.Linter.Style.SetOption.is_set_option stx = match Mathlib.Linter.Style.SetOption.parse_set_option stx with | some _name => true | x => false

def Mathlib.Linter.Style.SetOption.getLinterHash (o : Lean.Options) : Bool

Gets the value of the linter.setOption option.

Equations

• Mathlib.Linter.Style.SetOption.getLinterHash o = Lean.Linter.getLinterValue Mathlib.Linter.linter.setOption o

def Mathlib.Linter.Style.SetOption.setOptionLinter : Lean.Linter

The setOption linter: this lints any set_option command, term or tactic which sets a pp, profiler or trace option.

Why is this bad? These options are good for debugging, but should not be used in production code. How to fix this? Remove these options: usually, they are not necessary for production code. (Some tests will intentionally use one of these options; in this case, simply allow the linter.)

Equations

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