Lean4
/-- `SyntaxNodeKind`s that are mostly "formatting": mostly they are ignored
because we do not want the linter to spend time on them.
The nodes that they contain will be visited by the linter anyway.
The nodes that *follow* them, though, will *not* be visited by the linter.
-/
def stoppers : Std.HashSet Name :=
{ -- "properly stopper tactics": the effect of these tactics is to return a normal form
-- (or possibly be finishing tactics -- the ultimate normal form!
-- finishing tactics could equally well be considered as `flexible`, but as there is
-- no possibility of a follower anyway, it does not make a big difference.)
``Lean.Parser.Tactic.tacticSorry, ``Lean.Parser.Tactic.tacticRepeat_, ``Lean.Parser.Tactic.tacticStop_,
`Mathlib.Tactic.Abel.abelNF, `Mathlib.Tactic.Abel.tacticAbel_nf!__, `Mathlib.Tactic.RingNF.ringNF,
`Mathlib.Tactic.RingNF.tacticRing_nf!__, `Mathlib.Tactic.Group.group, `Mathlib.Tactic.FieldSimp.fieldSimp,
`finiteness_nonterminal,
-- "continuators": the *effect* of these tactics is similar the "properly stoppers" above,
-- though they typically wrap other tactics inside them.
-- The linter ignores the wrapper, but does recurse into the enclosed tactics
``Lean.Parser.Tactic.tacticSeq1Indented, ``Lean.Parser.Tactic.tacticSeq, ``Lean.Parser.Term.byTactic, `by,
``Lean.Parser.Tactic.tacticTry_, `choice, -- involved in `first`
``Lean.Parser.Tactic.allGoals, `Std.Tactic.«tacticOn_goal-_=>_», ``Lean.Parser.Tactic.«tactic_<;>_», ``cdotTk,
``cdot}
