fact: Definition genGoodFoo `{_ : Arbitrary Foo} (n : nat) := let fix aux_arb init_size size n := match size with | 0 => backtrack [(1, foo <- arbitrary ;; ret (Some foo))] | S _ => backtrack [(1, foo <- arbitrary ;; ret (Some foo))] end in fun sz => aux_arb sz sz n.
imports: QuickChick(QuickChick Tactics) String mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) List ExtLib.Structures.Monads