Re: [isabelle] primrec or fun


the tutorial is originally from 2001 so might use idioms not up to date now.

- Gergely
From: cl-isabelle-users-bounces at [cl-isabelle-users-bounces at] On Behalf Of Rustom Mody [rustompmody at]
Sent: Wednesday, May 11, 2016 1:37 PM
To: Joachim Breitner
Cc: cl-isabelle-users at
Subject: Re: [isabelle] primrec or fun

On Wed, May 11, 2016 at 4:31 PM, Joachim Breitner <breitner at> wrote:

> Dear Rusi,
> Am Mittwoch, den 11.05.2016, 16:18 +0530 schrieb Rustom Mody:
> > In
> >
> > the general advice seems to be:
> >
> > >
> > > *From a practitioner’s point of view, primrec is a lower-level tool
> that
> > > you usually do not need to worry about, and simply always use fun.*
> > >
> >
> > However when I see examples anywhere I see mostly primrec and not fun
> I’m not sure about the history of primrec and fun, but some of the
> examples might be from times when fun was not around, or not as good as
> it is now. Also, some tutorials/classes/courses might deliberately use
> primrec to force the student to be aware of the differences between
> primitive recursion and general recursion.

Ok if you say so :-)
However is from 2016 and still
heavily uses primrec?

[Sorry for being obtuse -- just finding it hard to find my way around]

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