fact: Fixpoint map_loop {T} {U A: choice_type} (s: seq T) (a: A) (c: T -> A -> raw_code (U × A)): raw_code (('seq U) × A) := match s with | [::] => ret (emptym, a) | t :: s' => ua1 ← c t a ;; ua2 ← map_loop s' ua1.2 c ;; ret (seq_to_chseq (ua1.1 :: unzip2 ua2.1), ua2.2) end.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)