Def Lean.ConstantVal.logOnUnusedInstancesInTypeWhere

Modification history

2026-10-06 14:58
Mathlib/Tactic/Linter/UnusedInstancesInType.lean
perf(Linter): bundle instance linters into one linter (#44436) …
Added Lean.ConstantVal.logOnUnusedInstancesInTypeWhereView on Github →