fact: Definition test (st : State) (f : nat -> RandomSeed -> QProp) : Result := if (gte (numSuccessTests st) (maxSuccessTests st)) then doneTesting st else if (gte (numDiscardedTests st) (maxDiscardedTests st)) then giveUp st else let maxSteps := maxSuccessTests st + maxDiscardedTests st in runATest st f maxSteps.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrnat ssrbool eqtype div) ExtLib(Structures.Monad) SimpleIO(SimpleIO) QuickChick(RoseTrees RandomQC Generators Producer SemChecker) QuickChick(Show Checker State Classes) Coq.Strings.Ascii Coq.Strings.String List Recdef Arith.EqNat