fact: Fixpoint mapFree {A B : choiceType} (f : A → B) (m : raw_code A) : raw_code B := match m with | ret x => ret (f x) | opr o x k => opr o x (λ r, mapFree f (k r)) | getr l k' => getr l (λ v, mapFree f (k' v)) | putr l v k' => putr l v (mapFree f k') | sampler op k' => sampler op (λ a, mapFree f (k' a)) end.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd RulesStateProb StateTransformingLaxMorph choice_type) Equations.Prop.DepElim Equations(Equations)