Xia Li-yao
Xia Li-yao
For some reason we only generate pairs where the list `s` is longer than the nat `n`!
The reason is that we use `genListSized` which generates lists of length equal to the current size. Maybe it should pick a random size? I'm not sure what the semantics...
Oh I see! Thanks @cpitclaudel !
Fair enough!
It seems fine to enable it. We can just make a new release with the patch though, right?
Patching things downstream until the next release (which should work for even Coq 8.11) sounds like a good plan. As far as opam is concerned, the git tag is the...
Maybe @lemonidas can tell what's going on. The anomaly actually comes from line 20. And on line 19 I also get ``` Cannot infer this placeholder of type "forall n1...
The best solution for QuickChick is probably to imitate Haskell QuickCheck with a splittable PRNG. The missing piece is an actual implementation of a splittable PRNG [that would go right...
`CoArbitrary` is also meant to generate functions, with better coverage and performance than key-value pairs when the domain `A` is large.
I'm not sure what's going on but the size parameter seems to be a confounding factor: ``` QuickChick (resize 10 (checker (fun m n : nat => implication (m collect...