fact: Fixpoint bind {A B} (c : raw_code A) (k : A → raw_code B) : raw_code B := match c with | ret a => k a | opr o x k' => opr o x (λ p, bind (k' p) k) | getr l k' => getr l (λ v, bind (k' v) k) | putr l v k' => putr l v (bind k' k) | sampler op k' => sampler op (λ a, bind (k' a) k) 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)