Leonidas Lampropoulos

The proof term derivation for generators is broken as of a couple of builds ago. The Computing Correctly derivations are much more robust (as they are proof scripts rather than...

Thanks for this! It will be great help in testing out our automatic derivation of Checkable instances. Such completely automatic derivation is still a bit further in the future, but...

Yeah, the problem is that mutually inductive types require mutually recursive functions. Currently, the plugin relies on typeclasses for resolving instances - but we can't just define two typeclass instances...

This is an interesting one. Basically, when we try to derive a generator for the third constructor, the process goes like this: - Figure out that the shape of the...

@Lysxia take a look at what I have over at [the dec-deriving branch](https://github.com/QuickChick/QuickChick/blob/dec-derivining/src/Producer.v). It might already fix your problems with GenLow as it reorganizes that part (and fixes/simplifies tons of...

Agreed on both counts. I had never noticed the former, but we knew of the reverse order. It has just been low priority as it's not actually breaking anything when...

There used to be such a [tactic](https://github.com/QuickChick/QuickChick/blob/master/src/tactic_quickchick.ml4), but it was (1) broken by the Coq 8.8 upgrade (2) fairly limited in scope. I can make fixing (1) a short-term priority...

I'll try and restore that tactic tomorrow then :)

It turns out this is a bit trickier than expected, since plugins can no longer introduce inconsistencies (which this tactic was doing: introducing the current goal as an axiom, and...

Must be a bug with implicit arguments. I'll take a look.