Re: [isabelle] primrec or fun



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

> Dear Rusi,
>
> Am Mittwoch, den 11.05.2016, 16:18 +0530 schrieb Rustom Mody:
> > In
> >
> http://stackoverflow.com/questions/30419419/what-is-the-difference-between-primrec-and-fun-in-isabelle-hol
> > 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 http://isabelle.in.tum.de/doc/tutorial.pdf 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.