Re: [isabelle] primcorec does not terminate
Thanks for the hint with quick_and_dirty. Now I can continue my work without having to
define the function manually.
On 16/04/15 21:19, Dmitriy Traytel wrote:
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.
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and