Def Mathlib.Command.MinImps.getIrredundantImports

Modification history

2024-07-21 13:36
Mathlib/Tactic/MinImports.lean
fix: handle nameless instances in `#min_imports in` (#14878) …
Deleted Mathlib.Command.MinImps.getIrredundantImportsView on Github →
2024-07-18 07:43
Mathlib/Tactic/MinImports.lean
feat: `#min_imports in` command (#14437) …
Added Mathlib.Command.MinImps.getIrredundantImportsView on Github →