Def Mathlib.Linter.getConcreteInstanceAssumptions

Modification history

2026-10-26 09:43
Mathlib/Tactic/Linter/DeclType.lean
feat(Linter): linter that detects concrete instances (#44625) …
Added Mathlib.Linter.getConcreteInstanceAssumptionsView on Github →