fact: Fixpoint gen_stack (n : nat) (onlyLow : bool) : G Stack := match n with | O => returnGen Mty | S n' => freq_ (returnGen Mty) [ (10, liftGen2 Cons gen_atom (gen_stack n' onlyLow)); (4, bindGen gen_atom (fun pc => liftGen (RetCons pc) (gen_stack n' (is_atom_low pc))))] end.
imports: QuickChick(QuickChick) ZArith List QuickChick.ifcbasic(Machine)