44a2b085c4
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> |
||
|---|---|---|
| .. | ||
| lib | ||
| AnalyzeGrindAnnotations.lean | ||
| apply.lean | ||
| bench.sh | ||
| benchReelabRss.lean | ||
| collideProfiles.lean | ||
| diff_changelogs.py | ||
| gen_constants_cpp.py | ||
| gen_tokens_cpp.py | ||
| issues_summary.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||
| mathlib-bench | ||
| merge_remote.py | ||
| Modulize.lean | ||
| patch.sh | ||
| prepare-llvm-linux.sh | ||
| prepare-llvm-macos.sh | ||
| prepare-llvm-mingw.sh | ||
| push_repo_release_tag.py | ||
| rebase-stage0.sh | ||
| reformat.lean | ||
| release_checklist.py | ||
| release_notes.py | ||
| release_repos.yml | ||
| release_steps.py | ||