Re: [Hol-info] RESTRICT left over in definition

Yes, I thought that was one of the more likely possible causes. Let me know if you can devise a better congruence rule that still gets the termination argument to go through. On 23 February 2016 at 15:40, Konrad Slind wrote: > Preliminary comment: the congruence rule

Re: [Hol-info] RESTRICT left over in definition

Preliminary comment: the congruence rule looks a bit suspect. I doubt the termination condition extractor is setup to deal with pairs in the concluding equality of a congruence rule. Konrad. On Mon, Feb 22, 2016 at 9:36 PM, Ramana Kumar wrote: > Hi Konrad, > >

Re: [Hol-info] RESTRICT left over in definition

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 wrote: > I have