Def Mathlib.Command.MinImports.getIds

Modification history

2024-07-21 13:36

Mathlib/Tactic/MinImports.lean

fix: handle nameless instances in `#min_imports in` (#14878) …

Added Mathlib.Command.MinImports.getIds View on Github →