The "commandRanges" linter

The "commandRanges" linter simply logs the getRange? and the getRangeWithTrailing? for each command.

This is useful for the "removeDeprecations" automation, since it helps identifying the exact range of each declaration that should be removed.

This linter is strictly tied to the #clear_deprecations command in Mathlib/Tactic/Linter/FindDeprecations.lean.

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

The "commandRanges" linter logs the getRange? and the getRangeWithTrailing? for each command. The format is [start, end, trailing], where

• start is the start of the command,
• end is the end of the command, not including trailing whitespace and comments,
• trailing is the "syntactic end" of the command, so it contains all trailing whitespace and comments.

Thus, assuming that there has been no tampering with positions/synthetic syntax, if the current command is followed by another command, then trailing for the previous command coincides with start of the following.

def Mathlib.Linter.CommandRanges.commandRangesLinter : Lean.Linter

The "commandRanges" linter logs the getRange? and the getRangeWithTrailing? for each command. The format is [start, end, trailing], where

• start is the start of the command,
• end is the end of the command, not including trailing whitespace and comments,
• trailing is the "syntactic end" of the command, so it contains all trailing whitespace and comments.

Thus, assuming that there has been no tampering with positions/synthetic syntax, if the current command is followed by another command, then trailing for the previous command coincides with start of the following.

Equations

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