Re: [isabelle] primrec of datatype containing fset
Sorry, I had missed your message. I fully agree with your disagreement. :-)
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Manuel Eberl <eberlm at in.tum.de>
Sent: 09 July 2017 12:54:12
To: cl-isabelle-users at lists.cam.ac.uk
Subject: Re: [isabelle] primrec of datatype containing fset
I don't fully agree.
There are some cases, like infinitely-branching datatypes, where
"primrec" works without problems, but "function" requires considerable
additional work (because there is no usable "size" function).
Also, for datatypes with many constructors, I think "function" can be
quite slow due to the huge number of things it does and theorems that it
proves. "primrec" is a good light-weight alternative then.
Personally, I tend to use primrec rather than fun whenever it is
possible to do so without significant effort.
On 2017-07-09 11:49, Lawrence Paulson wrote:
> 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