Commit 2026-10-23 11:07 da43ae12
View on Github →chore: modulize most of MathlibTest (#45134) (This is split off to cover the easy parts of #45122 that ought to be unproblematic) This PR modulize ~90% of all remaining unmodulized test files, this was done mostly using the Modulize.lean script from core. Some things beyond are changed (note all changes are in the test files!):
- Adapt some guard_msg (i.e. since line count changes) (4 files)
- sometimes meta for def/import is added, so #eval etc works (41 files)
- sometimes public keyword was added to defs instead of public section