fact: Definition ID (I : Interface) : raw_package := mkfmap [seq let '(n, p) := i in (n, let '(s, t) := p in mkdef s t (λ x, opr (n, (s, t)) x (λ y, ret y))) | i <- I ].
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)