Looks horrible. There shouldn't be remaining occurrences of RESTRICT.
Termination-condition extraction should remove them all.
Can you send me a cut-down version of the problematic function?
Konrad.
On Sun, Feb 21, 2016 at 5:34 AM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
wrote:
> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
