Commit 2024-05-26 13:31 6811a06d

View on Github →

feat: lint attribute [instance] instName in (#13190) Contrary to what users would expect, this defines a global instance. This linter would have caught #13144 and #13170. Zulip discussion Co-authored by: @adomani

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/Linter.lean

Created Mathlib/Tactic/Linter/AttributeInstanceIn.lean

added def Mathlib.Linter.attributeInstanceLinter.attributeInstanceIn

added def Mathlib.Linter.attributeInstanceLinter.getLinterAttributeInstanceIn

added def Mathlib.Linter.attributeInstanceLinter.is_attribute_instance_in

Modified Mathlib/Topology/Category/TopCat/Basic.lean

Created test/attributeInstanceIn.lean

added def bar

added def foo