RFC: Try this for #min_imports #698
Description
Proposal
Would it be possible to add a small button in VSCode extension for #min_imports, where clicking it automatically replaces all the imports with minimized imports? Probably adding Try this button will be more than enough (I always copy-paste manually.)
Community Feedback
Lean Zulip thread: #lean4 > Feature request - button to replace with minimized imports. Damiano Testa suggested further idea on adding "Try this".
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.