Zulip Chat Archive

Stream: new members

Topic: Examples for using slim_check testing?

Mike Hicks (Nov 14 2023 at 15:36):

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 (Nov 14 2023 at 16:35):

Here is a simple example

import Mathlib.Tactic

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

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.

Last updated: Dec 20 2023 at 11:08 UTC