Re: [isabelle] primcorec does not terminate



Hi Andreas,

in any case primcorec should always terminate. Here, you definition looks fine to me. It seems that one of the primcorec tactics is spinning. I guess we'll need Jasmin's expertise here when he is back from vacation.

Temporarily, you can use quick_and_dirty to get this definition through.

Best wishes,
Dmitriy



On 16.04.2015 17:06, Andreas Lochbihler wrote:
Dear BNF experts,

In the attached theory, the primcorec definition of a function does not terminate (tested with both Isabelle2014 and Isabelle2015-RC0). Is is because my definition is erroneous or a shortcoming of the primcorec implementation?

Best,
Andreas





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.