Re: [isabelle] Difference between primrec and fun

On 2 Oct 2019, at 10:18, Dominique Unruh <unruh at<mailto:unruh at>> 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.


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