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> 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.