Commit 2024-05-01 05:42 59710fc9

View on Github →

feat: make Fact testable for slim_check (#12566) Closes #12565 Also adds a sort-of-missing g.withContext. I don't think its absence causes any errors.

Estimated changes

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Tactic/SlimCheck.lean

Modified Mathlib/Testing/SlimCheck/Testable.lean

Modified test/slim_check.lean