I have managed to make a definition where the theorem returned to me by tDefine still contains occurrences of ``RESTRICT new_func (@R. WF R /\ ...)``.
Is this to be expected from tricky input equations, or is it a sign of a problem in the recursive function package? Would it be easy to post-process the resulting definition theorem to remove the RESTRICT? As is usual in such situations, there is a fair amount of context required to explore what's going on interactively, but if anyone is interested the relevant definition is made here: https://github.com/machine-intelligence/Botworld.HOL/blob/37747faa1eda333086612101023803967a8645e5/botworld_quoteScript.sml#L135 ------------------------------------------------------------------------------ Site24x7 APM Insight: Get Deep Visibility into Application Performance APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month Monitor end-to-end web transactions and take corrective actions now Troubleshoot faster and improve end-user experience. Signup Now! http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140 _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
