Lean4
/-- `SyntaxNodeKind`s that are allowed to follow a flexible tactic:
`simp`, `simp_all`, `simpa`, `dsimp`, `grind`, `constructor`, `congr`, `done`, `rfl`,
`omega` and `cutsat`, `grobner`
`abel` and `abel!`, `group`, `ring` and `ring!`, `module`, `field_simp`, `norm_num`,
`linarith`, `nlinarith` and `nlinarith!`, `norm_cast`, `tauto`,
`aesop`, `cfc_tac` (and `cfc_zero_tac` and `cfc_cont_tac`),
`continuity` and `measurability`, `finiteness`, `finiteness?`,
`split`, `split_ifs`.
-/
def flexible : Std.HashSet Name :=
{``Lean.Parser.Tactic.simp, ``Lean.Parser.Tactic.simpAll, ``Lean.Parser.Tactic.simpa, ``Lean.Parser.Tactic.dsimp,
``Lean.Parser.Tactic.constructor, ``Lean.Parser.Tactic.congr, ``Lean.Parser.Tactic.done,
``Lean.Parser.Tactic.tacticRfl, ``Lean.Parser.Tactic.omega, `Mathlib.Tactic.Abel.abel,
`Mathlib.Tactic.Abel.tacticAbel!, `Mathlib.Tactic.Group.group, `Mathlib.Tactic.RingNF.ring,
`Mathlib.Tactic.RingNF.tacticRing!, `Mathlib.Tactic.Module.tacticModule, `Mathlib.Tactic.FieldSimp.fieldSimp,
``Lean.Parser.Tactic.grind, ``Lean.Parser.Tactic.grobner, ``Lean.Parser.Tactic.cutsat, `Mathlib.Tactic.normNum,
`Mathlib.Tactic.linarith, `Mathlib.Tactic.nlinarith, `Mathlib.Tactic.tacticNlinarith!_,
`Mathlib.Tactic.LinearCombination.linearCombination, ``Lean.Parser.Tactic.tacticNorm_cast__,
`Aesop.Frontend.Parser.aesopTactic,
-- `cfc_tac` and `cfc_zero_tac` use `aesop` under the hood,
-- `cfc_cont_tactic` uses `fun_prop`: in practice, this should be robust enough.
`cfcTac, `cfcZeroTac, `cfcContTac,
-- `continuity` and `measurability` also use `aesop` under the hood.
`tacticContinuity, `tacticMeasurability, `finiteness, `finiteness?, `Mathlib.Tactic.Tauto.tauto,
`Lean.Parser.Tactic.split, `Mathlib.Tactic.splitIfs}
