fact: Definition resultSuccessful (r : Result) : bool := match r with | MkResult (Some res) expected _ _ _ _ _ => res == expected | _ => true end.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes