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.