Commit 2026-03-25 22:20 275ec219

View on Github →

chore: modulize tests (4/N) (#36981)

Estimated changes

Modified MathlibTest/Change.lean

Modified MathlibTest/ClearExcept.lean

Modified MathlibTest/ClearExclamation.lean

Modified MathlibTest/ClearValue.lean

Modified MathlibTest/Clear_.lean

Modified MathlibTest/Constructor.lean

Modified MathlibTest/Contrapose.lean

Modified MathlibTest/EmptyLine.lean

Modified MathlibTest/Equiv.lean

Modified MathlibTest/ErwQuestion.lean

Modified MathlibTest/ImplicitUniverses.lean

Modified MathlibTest/InferParam.lean

Modified MathlibTest/IsBoundedDefault.lean

Modified MathlibTest/MoveAdd.lean

Modified MathlibTest/NoncommRing.lean

Modified MathlibTest/NthRewrite.lean

Modified MathlibTest/PPRoundtrip.lean

Modified MathlibTest/ProdAssoc.lean

Modified MathlibTest/Rename.lean

Modified MathlibTest/Simp.lean

Modified MathlibTest/SwapVar.lean

Modified MathlibTest/TermCongr.lean

Modified MathlibTest/TermCongr2.lean

Modified MathlibTest/UnusedTactic.lean

Modified MathlibTest/apply_congr.lean

Modified MathlibTest/apply_rules.lean

Modified MathlibTest/apply_with.lean

Modified MathlibTest/basicTactics.lean

Modified MathlibTest/byContra.lean

Modified MathlibTest/cases.lean

Modified MathlibTest/choose_reduction.lean

Modified MathlibTest/coe.lean

Modified MathlibTest/conv.lean

Modified MathlibTest/enat_to_nat.lean

Modified MathlibTest/norm_num_flt.lean

Modified MathlibTest/norm_num_ordinal.lean

Modified MathlibTest/norm_num_rpow.lean

Modified MathlibTest/reduce_mod_char.lean

Modified MathlibTest/renameBvar.lean

Modified MathlibTest/right_actions.lean

Modified MathlibTest/wlog.lean