fact: Definition cmd_bind {A B} (c : command A) (k : A → raw_code B) := match c in command A return (A → raw_code B) → raw_code B with | cmd_op o x => opr o x | cmd_get ℓ => getr ℓ | cmd_put ℓ v => λ k, putr ℓ v (k Datatypes.tt) | cmd_sample op => sampler op end k.
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)