usesGoal? — Mathlib

Lean4
/-- By default, if a `SyntaxNodeKind` is not special-cased here, then the linter assumes that
the tactic will use the goal as well: this heuristic works well with `exact`, `refine`, `apply`.
For tactics such as `cases` this is not true: for these tactics, `usesGoal?` yields `false. -/
def usesGoal? : SyntaxNodeKind → Bool
  | ``Lean.Parser.Tactic.cases => false
  | `Mathlib.Tactic.cases' => false
  | ``Lean.Parser.Tactic.obtain => false
  | ``Lean.Parser.Tactic.tacticHave__ => false
  | ``Lean.Parser.Tactic.rcases => false
  | ``Lean.Parser.Tactic.specialize => false
  | ``Lean.Parser.Tactic.subst => false
  | ``«tacticBy_cases_:_» => false
  | ``Lean.Parser.Tactic.induction => false
  | _ => true
Похожие утверждения