Lean4
@[command_elab Mathlib.Command.MinImports.minImpsStx]
public meta def _aux_Mathlib_Tactic_MinImports___elabRules_Mathlib_Command_MinImports_minImpsStx_1 :
Lean.Elab.Command.CommandElab✝ := fun
| `(#min_imports in $cmd:command) => do
-- In case `cmd` is a "nameless" `instance`, we produce its name.
-- It is important that this is collected *before* adding the declaration to the environment,
-- since `getId` probes the name-generator using the current environment: if the declaration
-- were already present, `getId` would return a new name that does not clash with it!
let id ← getId cmd
Elab.Command.elabCommand cmd <|> pure ()
minImpsCore cmd id
| _ => no_error_if_unused% throwUnsupportedSyntax✝
