Def Mathlib.Command.MinImports.getAllDependencies

Modification history

2024-11-18 11:19
Mathlib/Tactic/MinImports.lean
feat: the upstreamDecl linter (#18702) …
Added Mathlib.Command.MinImports.getAllDependenciesView on Github →