Examples for using slim_check testing?

Stream: new members

[Mike Hicks]

I'm familiar with QuickChick for Coq and I believe that SlimCheck provides similar functionality for Lean.

Are there examples anywhere of its use? A small "get started" example would be super helpful.

And: Can anyone comment on important gaps in the current codebase? I see that commits to it are fairly recent so perhaps gaps that were flagged by other threads back in March are resolved.

[Alex J. Best]

Here is a simple example

import Mathlib.Tactic

example (l : Nat × Nat) (h : 2 ≤ l.1 + l.2) : 1 ≤ l.1 := by
  slim_check

slim_check informs me that my goal is unprovable and provides a counterexample
https://github.com/leanprover-community/mathlib4/blob/master/test/slim_check.lean lists many more examples. You can see there that some are commented out, which may be due to missing functionality.