getTactics

Mathlib.Tactic.Linter.UnusedTactic

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.UnusedTactic.getTactics

Lean4

/-- Accumulates the set of tactic syntaxes that should be evaluated at least once. -/
@[specialize]
partial def getTactics (stx : Syntax) : M Unit := do
  if let .node _ k args := stx then
    if !isIgnoreTacticKind ignoreTacticKinds k then
      args.forM getTactics
    if isTacKind k then
      if let some r := stx.getRange? true then
        modify fun m => m.insert r stx

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru