Commit 2023-05-10 06:12 07745762

View on Github →

feat: tactic frontend for slim_check (#3114) Adds a tactic front end for slim_check, and provides commands #test and #sample. Updates all the mathlib3 tests, although many are broken. There are still some missing parts of Mathlib.Testing.SlimCheck.Sampleable: in particular we can't currently sample from lists, and this explains most of the broken tests.

Estimated changes