fact: Definition callbackPostTest (st : State) (res : Checker.Result) : nat := match res with | MkResult o e r i s c t => fold_left (fun acc callback => match callback with | PostTest _ call => (call st (MkSmallResult o e r i s t)) + acc | _ => acc end) c 0 end.
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