Re: [isabelle] Primrec abstracts over the wrong variable



Dear primrec user,

Thank you for your report. I have now solved the issue in primrec so that your example should work in the next Isabelle release. I'm glad you have a workaround in the meantime.

Cheers,

Jasmin

> On 17 May 2021, at 15:26, Andreas Lochbihler <mail at andreas-lochbihler.de> wrote:
> 
> Dear primrec experts,
> 
> In the attached theory for Isabelle2021, I'm trying to define a simple primitively recursive function over a datatype. However, primrec complains about "extra variables on rhs" in the underlying foundational definition. It looks to me as if primrec does not correctly construct the lambda abstraction for the second argument to the recursor. My current workaround is to use fun instead, but it would be nice to get the support for transfer rules from primrec.
> 
> Best,
> Andreas
> <Scratch.thy>





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