Commit 2024-07-18 07:43 9ef349ab
View on Github →feat: #min_imports in command (#14437)
This PR introduces the #min_imports in command.
Writing #min_imports in stx scans the syntax stx to find a collection of minimal imports that should be sufficient for stx to make sense.
If stx is a command, then it also elaborates stx. If stx produces a declaration, then
it also finds the imports implied by the declaration.
Unlike the related #find_home, this command takes into account notation and tactic information.
For instance, you can write
import Mathlib
#min_imports in
lemma hi (n : ℕ) : n = n := by extract_goal; rfl
-- import Mathlib.Tactic.ExtractGoal
-- import Mathlib.Tactic.Lemma
-- import Mathlib.Init.Data.Nat.Notation
and you can see that it notices lemma, ℕ and extract_goal.