Re: [isabelle] Difference between primrec and fun



On 2 Oct 2019, at 10:18, Dominique Unruh <unruh at ut.ee<mailto:unruh at ut.ee>> wrote:


Thanks for your answers.

So, as an executive summary of the executive summary (including Manuel's answer), we could say: There are cases where primrec works and fun doesn't and vice versa. And if both work, use primrec because it's faster and some things might be easier later.

Please correct me if that rule of thumb is wrong.

Sounds reasonable to me.

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.

Cheers,
Dmitriy



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