Lean4
/-- The `SyntaxNodeKind`s in `exclusions` correspond to tactics that the linter allows,
even though there are multiple active goals.
Reasons for admitting a kind in `exclusions` include
* the tactic focuses on one goal, e.g. `·`, `focus`, `on_goal i =>`, ...;
* the tactic is reordering the goals, e.g. `swap`, `rotate_left`, ...;
* the tactic is structuring a proof, e.g. `skip`, `<;>`, ...;
* the tactic is creating new goals, e.g. `constructor`, `cases`, `induction`, ....
There is some overlap in scope between `ignoreBranch` and `exclusions`.
Tactic combinators like `repeat` or `try` are a mix of both.
-/
abbrev exclusions : Std.HashSet SyntaxNodeKind :=
.ofArray
#[
-- structuring a proof
``Lean.Parser.Term.cdot, ``cdot, ``cdotTk, ``Lean.Parser.Tactic.tacticSeqBracketed, `«;», `«<;>»,
``Lean.Parser.Tactic.«tactic_<;>_», `«{», `«]», `null, `then, `else, ``Lean.Parser.Tactic.«tacticNext_=>_»,
``Lean.Parser.Tactic.tacticSeq1Indented, ``Lean.Parser.Tactic.tacticSeq,
-- re-ordering goals
`Batteries.Tactic.tacticSwap, ``Lean.Parser.Tactic.rotateLeft, ``Lean.Parser.Tactic.rotateRight,
``Lean.Parser.Tactic.skip, `Batteries.Tactic.«tacticOn_goal-_=>_», `Mathlib.Tactic.«tacticSwap_var__,,»,
-- tactic combinators
``Lean.Parser.Tactic.tacticRepeat_, ``Lean.Parser.Tactic.tacticTry_,
-- creating new goals
``Lean.Parser.Tactic.paren, ``Lean.Parser.Tactic.case, ``Lean.Parser.Tactic.constructor,
`Mathlib.Tactic.tacticAssumption', ``Lean.Parser.Tactic.induction, ``Lean.Parser.Tactic.cases,
``Lean.Parser.Tactic.intros, ``Lean.Parser.Tactic.injections, ``Lean.Parser.Tactic.substVars,
`Batteries.Tactic.«tacticPick_goal-_», ``Lean.Parser.Tactic.case', `«tactic#adaptation_note_»,
`tacticSleep_heartbeats_]
