Re: [isabelle] primrec of datatype containing fset



These days, users should regard "primrec" as an internal feature necessary for bootstrapping the system but for implementers only.

Larry Paulson


> On 9 Jul 2017, at 11:15, Lars Hupel <hupel at in.tum.de> wrote:
> 
> this is a restriction of "primrec". What you're writing is not in fact a
> primitive recursive specification. There are two ways around that:
> 
> 1) Rewrite it as primitive recursive
> 2) Use the "fun"/"function" command





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