The "multiGoal" linter

The "multiGoal" linter emits a warning where there is more than a single goal in scope. There is an exception: a tactic that closes all remaining goals is allowed.

There are a few tactics, such as skip, swap or the try combinator, that are intended to work specifically in such a situation. Otherwise, the mathlib style guide ask that goals be focused until there is only one active goal at a time. If this focusing does not happen, the linter emits a warning. Typically, the focusing is achieved by the cdot: ·, but, e.g., focus or on_goal x also serve a similar purpose.

TODO:

• Should the linter flag unnecessary scoping as well? For instance, should

  example : True := by
    · · exact .intro
  

  raise a warning?
• Custom support for "accumulating side-goals", so that once they are all in scope they can be solved in bulk via all_goals or a similar tactic.
• In development, on_goal has been partly used as a way of silencing the linter precisely to allow the accumulation referred to in the previous item. Maybe revisit usages of on_goal and also nested induction and cases.

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

The "multiGoal" linter emits a warning when there are multiple active goals.