Commit 2023-09-20 04:57 2c3ee375
View on Github →chore(test/*): add test_sorry axiom in tests to make them less noisy (#6868)
This PR adds axiom test_sorry for the sorrys in tests, in order to remove the noisy output of sorry.
In test/rewrites.lean and test/IsCompact.lean some of the #guard_msgs are #guard_msgs(warning), due to further messages.
Affected files:
test/apply_fun.lean
test/cancel_denoms.lean
test/Change.lean
test/congr.lean
test/congrm.lean
test/convert.lean
test/DefEqTransformations.lean
test/FBinop.lean
test/GCongr/inequalities.lean
test/GeneralizeProofs.lean
test/ImplicitUniverses.lean
test/InstanceTransparency.lean
test/LibrarySearch/IsCompact.lean
test/LiftLets.lean
test/linarith.lean
test/MfldSetTac.lean
test/mod_cases.lean
test/Monotonicity.lean
test/nontriviality.lean
test/norm_num.lean
test/push_neg.lean
test/Real.lean
test/rewrites.lean
test/ring.lean
test/Zify.lean