Commit 2026-10-26 09:43 8d14a323

feat(Linter): linter that detects concrete instances (#44625) This PR implements a linter that flags concrete instances. This is useful for beginners who might write [Field ℝ] because they want to use that ℝ is a field. There is a built in exception for Decidable, since adding redundant Decidable hypotheses, such as DecidableEq True and ∀ P, Decidable P, can be desired to avoid instance diamonds.