fact: Fixpoint code_link {A} (v : raw_code A) (p : raw_package) : raw_code A := match v with | ret a => ret a | opr o a k => match lookup_op p o with | Some f => bind (f a) (λ x, code_link (k x) p) | None => code_link (k (chCanonical (chtgt o))) p end | getr l k => getr l (λ x, code_link (k x) p) | putr l v k => putr l v (code_link k p) | sampler op k => sampler op (λ x, code_link (k x) p) end.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool ssrnat) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd StateTransformingLaxMorph choice_type pkg_core_definition RulesStateProb) Equations(Equations)