Lean4
/-- The `SyntaxNodeKind`s in `ignoreBranch` correspond to tactics that disable the linter from
their first application until the corresponding proof branch is closed.
Reasons for ignoring these tactics include
* the linter gets confused by the proof management, e.g. `conv`;
* the tactics are *intended* to act on multiple goals, e.g. `repeat`, `any_goals`, `all_goals`, ...
There is some overlap in scope between `exclusions` and `ignoreBranch`.
-/
abbrev ignoreBranch : Std.HashSet SyntaxNodeKind :=
.ofArray
#[``Lean.Parser.Tactic.Conv.conv, `Mathlib.Tactic.Conv.convLHS, `Mathlib.Tactic.Conv.convRHS,
``Lean.Parser.Tactic.first, ``Lean.Parser.Tactic.repeat', ``Lean.Parser.Tactic.tacticIterate____,
``Lean.Parser.Tactic.anyGoals, ``Lean.Parser.Tactic.allGoals, ``Lean.Parser.Tactic.focus,
``Lean.Parser.Tactic.failIfSuccess, `Mathlib.Tactic.successIfFailWithMsg]
