Re: [isabelle] primcorec does not terminate



Hi Dmitriy,

Thanks for the hint with quick_and_dirty. Now I can continue my work without having to define the function manually.

Best,
Andreas

On 16/04/15 21:19, Dmitriy Traytel wrote:
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.