Leonidas Lampropoulos

Unfortunately, this is caused by Coq's extraction mechanism, not us. As long as QuickChick needs to rely on extraction for randomness and performance, this is the expected behavior.

Revisiting this, if we want to eventually derive executable content out of inductive relations, the easiest way would be to provide two classes: * Something like the decidable class we...

You're right, it's the extraction unsoundness that yields this "counter-example". I'm not sure what the best way to address this moving forward is (so @Lysxia @liyishuai I'd like your thoughts!):...

My victory sign appeared because the proof that my translation from positives to split paths (lists of 0/1 signifying (fst . split) / (snd . split)) is prefix free took...

One solution could be to make frequency take thunks `fun (_ : unit) => ...` and use the `freq` notation already in place to ensure the user never actually sees...

Is it really more efficient to use thunkGen everywhere instead of bind? A good compromise would be to have thunked generators in all combinators that take multiple generators as arguments...

sigh Great catch. Maybe redesign the main API functions for 2.0? I'm gearing up towards its release soon.

ExtLib also provides a [Show module](https://github.com/coq-ext-lib/coq-ext-lib/blob/master/theories/Programming/Show.v). Any thoughts on that?

I agree that S-expressions do seem like a straightforward target for the derivation procedure. > I'm also not a fan of big libraries in the style of ext-lib in general:...

Should QuickChick be made to depend on that? As long as the Coq CI is happy, I'm happy. The current plan seems to be to only move the "Show" definitions...