Zulip Chat Archive
Stream: new members
Topic: optimize imports
Wouter Smeenk (Jul 16 2023 at 11:28):
Is there a way to optimize the import. Select the minimal set of imports?
Yury G. Kudryashov (Jul 16 2023 at 15:27):
Try #minimize_imports
Yury G. Kudryashov (Jul 16 2023 at 15:27):
It's a Lean 4 addition, I never tried.
Last updated: May 02 2025 at 03:31 UTC