fact: Definition disjAux (p q : Rose Result) : Rose Result := joinRose (fmapRose' p (fun result1 => if expect result1 then match ok result1 with | Some true => returnRose result1 | Some false => joinRose (fmapRose' q (fun result2 => if expect result2 then match ok result2 with | Some true => returnRose result2 | Some false => returnRose (MkResult (ok result2) (expect result2) (if string_dec (reason result2) EmptyString then reason result1 else reason result2) (orb (interrupted result1) (interrupted result2)) (stamp result1 ++ stamp result2) (callbacks result1 ++ cons (PostFinalFailure Counterexample (fun _ _ => trace newline 0)) nil ++ callbacks result2 ) (result_tag result2)) | None => returnRose result2 end else returnRose expectFailureError)) | None => joinRose (fmapRose' p (fun result2 => if expect result2 then match ok result2 with | Some true => returnRose result2 | _ => returnRose result1 end else returnRose expectFailureError)) end else returnRose expectFailureError)).
imports: String List RoseTrees Show State Producer Generators Classes DependentClasses