fact: Fixpoint backtrackFuel {A : Type} (fuel : nat) (tot : nat) (gs : list (nat * G (option A))) : G (option A) := match fuel with | O => ret None | S fuel' => bindGen (choose (0, tot-1)) (fun n => let '(k, g, gs') := pickDrop gs n in bindGen g (fun ma => match ma with | Some a => ret (Some a) | None => backtrackFuel fuel' (tot - k) gs' end )) end.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)