globalAttributeIn — Mathlib

Lean4
/-- The `globalAttributeInLinter` linter flags any global attributes generated by an
`attribute [...] in` declaration. (This includes the `instance`, `simp` and `ext` attributes.)

Despite the `in`, these define *global* instances, which can be rather misleading.
Instead, remove the `in` or mark them with `local`.
-/
def globalAttributeIn : Linter where
  run :=
    withSetOptionIn fun stx => do
      unless getLinterGlobalAttributeIn (← getLinterOptions) do
        return
      if (← MonadState.get).messages.hasErrors then
        return
      for s in stx.topDown do
        if let some (id, nonScopedNorLocal) := getGlobalAttributesIn? s then
          for attr in nonScopedNorLocal do
            Linter.logLint linter.globalAttributeIn attr
                m! "Despite the `in`, the attribute '{attr }' is added globally to '{id }'\n\
                            please remove the `in` or make this a `local {attr}`"
Похожие утверждения