Anything like QuickCheck

Stream: lean4

[Chris Lovett]

The https://mmhaskell.com/monads/laws at the end mentions a handy tool named QuickCheck. Does Lean have an equivalent?

[Mauricio Collares]

SlimCheck is in mathlib4 at the moment, but it might be moved elsewhere in the near future (perhaps to the newly-created std4?)

[Matthew Ballard]

Last I saw #lean4 > Where should SlimCheck/QuickCheck be? it was in mathlib4

[Mauricio Collares]

QuickCheck is still useful in Lean, but a big difference between Haskell and Lean is that in Lean you can prove that your monads are lawful (e.g., https://github.com/leanprover/lean4/blob/0925051c51e183a0b8c504ae53f5cab0525d6cac/src/Init/Control/Lawful.lean#L298-L307)

[Matej Penciak]

As mentioned in the above thread the Slimcheck parts of mathlib4 were copied into a separate testing repository LSpec (https://github.com/yatima-inc/LSpec) which is itself a port of Haskell's Hspec. Currently the documentation for the SlimCheck integration with LSpec isn't written down, but I'm planning on spelling it out in the next couple days