Commit 2026-10-05 11:29 b59261d2

View on Github →

chore(Linter): remove the upstreamed globalAttributeIn (#44499) The globalAttributeIn linter was upstreamed to Lean core in https://github.com/leanprover/lean4/pull/13223, so this PR removes it from Mathlib, to remove the duplication.

Estimated changes

Modified Mathlib/Init.lean

Modified Mathlib/Tactic/Linter/GlobalAttributeIn.lean

deleted def Mathlib.Linter.globalAttributeInLinter.getGlobalAttributesIn?

deleted def Mathlib.Linter.globalAttributeInLinter.getLinterGlobalAttributeIn

deleted def Mathlib.Linter.globalAttributeInLinter.globalAttributeIn

Deleted MathlibTest/Linter/GlobalAttributeIn.lean

deleted def X.bar

deleted theorem X.foo

deleted def dummyInst