Re: [isabelle] Difference between primrec and fun



> On 3 Oct 2019, at 10:57, Traytel Dmitriy <traytel at inf.ethz.ch> wrote:
> 
> > I think it might be useful to cover primrec in the function definition tutorial.
> 
> It is covered in the "datatypes" tutorial. It belongs there logically, because as Larry wrote, primrec is a relatively thin layer around the datatype's recursion combinator. But indeed a reference in the "functions" tutorial would make sense.

I'm not in charge of the "functions" tutorial, but a reference the other way does make sense. We already mentioned fun/function in the "datatypes" tutorial, but now I've just added (Isabelle/13d6b561b0ea) a paragraph capturing the essence of this thread.

Jasmin





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