Xia Li-yao

As far as I can tell, the only way around is to implement instances by hand, until someone extends the plugin accordingly.

My use case right now is to derive serialization functions (roughly Haskell's `Show` or Rust's `Debug`), so the context and types are not known statically to allow me to quote...

The fruit of my labor is here, hopefully that gives you a more concrete idea of where I'm coming from: - Some generic defintions (inncluding `tMatch`): https://github.com/Lysxia/coq-ceres/blob/a9cd1d750f9fd3ce67e2d98b92a7355baa88d091/theories/TemplateLib.v - Deriving a...

Actually `bindGen'` is still there, https://github.com/QuickChick/QuickChick/blob/e008077c093e5d20403f5067392a4206c5474246/src/GenLowInterface.v#L91-L92 I don't know why I added this comment https://github.com/QuickChick/QuickChick/blob/e008077c093e5d20403f5067392a4206c5474246/src/GenLowInterface.v#L50 The rest of the suggestion still stands though.

- [x] Finish the choose correctness proof - [x] Use the standard extraction for `uint63`

Refactoring the extraction logic out to coq-simple-io breaks the `make`-based build for currently released versions of Coq (it will hopefully be fixed in 8.16), so I'm switching everything to dune....

It would be nice to have every call to `newRandomSeed` generate a new seed. It should be a value of an abstract `IO` data type, rather than a Gallina function,...

I have a branch with a pure generator, that addresses this issue about `randomNext` (and `randomSplit`). I'm waiting for a release focusing on 8.8 compatibility to be done first before...

@djeis97 Sure! It's mostly that everyone's been too busy with other projects to work on QuickChick. One solution seems to be to revive the tactic mentioned in the discussion above,...

Can you try with this patch #223