fact: Definition lookup_op (p: raw_package) (o : opsig) : option (src o → raw_code (tgt o)) := let '(n, (So, To)) := o in match p n with | Some (St ; Tt ; f) => match choice_type_eqP St So, choice_type_eqP Tt To with | ReflectT hS, ReflectT hT => Some (cast_fun hS hT f) | _,_ => None end | None => None 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)