Commit 2026-04-05 12:58 63868fe5

View on Github →

chore: modulize tests (5/N) (#37654)

Estimated changes

Modified MathlibTest/CategoryTheory/PrettyPrinting.lean

Modified MathlibTest/DefEqAbuse.lean

Modified MathlibTest/DefEqTransformations.lean

Modified MathlibTest/FBinop.lean

Modified MathlibTest/FunLike.lean

Modified MathlibTest/InstanceTransparency.lean

Modified MathlibTest/Linarith/Basic.lean

deleted def testSorryTac

added def tightlyWrapped

Modified MathlibTest/Linarith/NNReal.lean

Modified MathlibTest/Monotonicity.lean

Modified MathlibTest/Replace.lean

Modified MathlibTest/SimpRw.lean

Modified MathlibTest/Subsingleton.lean

Modified MathlibTest/Zify.lean

Modified MathlibTest/abel.lean

added def MyTrue

Modified MathlibTest/apply_fun.lean

Modified MathlibTest/cancel_denoms.lean

Modified MathlibTest/congr.lean

Modified MathlibTest/congrm.lean

Modified MathlibTest/convert.lean

Modified MathlibTest/convert2.lean

Modified MathlibTest/itauto.lean

Modified MathlibTest/linear_combination'.lean

Modified MathlibTest/linear_combination.lean

Modified MathlibTest/mod_cases.lean

Modified MathlibTest/norm_num.lean

Modified MathlibTest/norm_num_abs.lean

Modified MathlibTest/push.lean

Modified MathlibTest/push_neg.lean

Modified MathlibTest/set_like.lean