The commandStart linter

The commandStart linter emits a warning if

• either a command does not start at the beginning of a line;
• or the "hypotheses segment" of a declaration does not coincide with its pretty-printed version.

opaque Mathlib.Linter.linter.style.commandStart : Lean.Option Bool

The commandStart linter emits a warning if

• either a command does not start at the beginning of a line;
• or the "hypotheses segment" of a declaration does not coincide with its pretty-printed version.

In practice, this makes sure that the spacing in a typical declaration looks like

example (a : Nat) {R : Type} [Add R] : <not linted part>

as opposed to

example (a: Nat) {R:Type}  [Add  R] : <not linted part>

opaque Mathlib.Linter.linter.style.commandStart.verbose : Lean.Option Bool

If the linter.style.commandStart.verbose option is true, the commandStart linter reports some helpful diagnostic information.

def Mathlib.Linter.Style.CommandStart.mkWindow (orig : String) (start ctx : Nat) : String

mkWindow orig start ctx extracts from orig a string that starts at the first non-whitespace character before start, then expands to cover ctx more characters and continues still until the first non-whitespace character.

In essence, it extracts the substring of orig that begins at start, continues for ctx characters plus expands left and right until it encounters the first whitespace character, to avoid cutting into "words".

Note. start is the number of characters from the right where our focus is!

Equations

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