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

Estimated changes

deleted def foo
deleted def leaky
deleted def unknownTacticTest
deleted def verifyFakeRfl