scripts/Modulize.lean
This PR introduces a simple script that adjusts module headers in a package for use of the module system, without further minimizing import or annotation use. --------- Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
