fact: Fixpoint bounded_do_while (n : nat) (c : MFreePr bool_choiceType) : MFreePr bool_choiceType := match n with | 0 => ord_relmon_unit MFreePr _ false | S n => ord_relmon_bind MFreePr (fun b => match b with | false => ord_relmon_unit MFreePr _ true | true => bounded_do_while n c end ) c end.
imports: Coq(RelationClasses Morphisms Utf8) Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod)