minImpsCore — Mathlib

Lean4
/-- `minImpsCore stx id` is the internal function to elaborate the `#min_imports in` command.
It collects the irredundant imports to parse and elaborate `stx` and logs
```lean
import A
import B
...
import Z
```
The `id` input is expected to be the name of the declaration that is currently processed.
It is used to provide the internally generated name for "nameless" `instance`s.
-/
def minImpsCore (stx id : Syntax) : CommandElabM Unit := do
  let tot := getIrredundantImports (← getEnv) (← getAllImports stx id)
  let fileNames := tot.toArray.qsort Name.lt
  logInfoAt (← getRef) m!"{"\n".intercalate (fileNames.map (s!"import {·}")).toList}"
Похожие утверждения