flexible?

Mathlib.Tactic.Linter.FlexibleLinter

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.flexible?

Lean4

/-- `flexible? stx` is `true` if `stx` is syntax for a tactic that takes a "wide" variety of
inputs and modifies them in possibly unpredictable ways.

The prototypical flexible tactic is `simp`.
The prototypical non-flexible tactic `rw`.
`simp only` is also non-flexible. -/
--  TODO: adding more entries here, allows to consider more tactics to be flexible

def flexible? : Syntax → Bool
  | .node _ ``Lean.Parser.Tactic.simp #[_, _, _, only?, _, _] => only?[0].getAtomVal != "only"
  | .node _ ``Lean.Parser.Tactic.simpAll #[_, _, _, only?, _] => only?[0].getAtomVal != "only"
  | _ => false

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

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

Разделы

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

Аффилиация

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