Commit 2024-07-21 13:36 02418396

View on Github →

fix: handle nameless instances in #min_imports in (#14878) This PR makes #min_imports in process better "nameless" instances, as well as attributes in declarations.

Estimated changes

Modified Mathlib/Tactic/MinImports.lean

added def Mathlib.Command.MinImports.getAllImports

added def Mathlib.Command.MinImports.getAttrNames

added def Mathlib.Command.MinImports.getAttrs

added def Mathlib.Command.MinImports.getId

added def Mathlib.Command.MinImports.getIds

added def Mathlib.Command.MinImports.getIrredundantImports

added def Mathlib.Command.MinImports.getSyntaxNodeKinds

added def Mathlib.Command.MinImports.getVisited

added def Mathlib.Command.MinImports.minImpsCore

deleted def Mathlib.Command.MinImps.getAllImports

deleted def Mathlib.Command.MinImps.getId

deleted def Mathlib.Command.MinImps.getIrredundantImports

deleted def Mathlib.Command.MinImps.getSyntaxNodeKinds

deleted def Mathlib.Command.MinImps.getVisited

deleted def Mathlib.Command.MinImps.minImpsCore

Modified test/MinImports.lean